Theorem ralbidv 1663

Description: Formula-building rule for restricted universal quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
ralbidv	|- (ph -> (A.x e. A ps <-> A.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	ralbid 1661	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146  A.wral 1645

This theorem is referenced by:  2ralbidv 1680  rexralbidv 1682  raleqd 1791  raleq12d 1794  cbvral2v 1803  rcla42v 1880  rcla43v 1882  reu7 1935  sbcralt 1990  sbcralgf 1992  raaan 2360  elintg 2541  elintrabg 2546  eliin 2571  poeq1 2842  dffr2 2919  wereu 2945  onssmin 3008  ralxpf 3220  cnvpo 3522  funcnvuni 3564  dff3 3818  f1fvf 3875  isowe 3903  f1oweALT 3906  tfrlem3 3913  tfrlem12 3922  rdgeq1 3934  rdgeq2 3935  tz7.48lem 3955  elixp2 4349  nneneq 4512  supeq1 4575  supmo 4576  supub 4580  suplub 4581  supmaxlem 4588  suppr 4590  supsnALT 4592  zfregcl 4595  unbnnt 4639  rankval3 4681  unbndrank 4683  rankuni2 4690  rankun 4691  scottex 4716  scottexs 4718  scott0s 4719  bnd2 4724  hta 4728  aceq4 4734  aceq5lem5 4739  aceq5 4740  aceq6a 4741  aceq6b 4742  kmlem2 4766  kmlem13 4777  zorn2lem2 4789  zorn2lem7 4794  zorn2 4796  brdom3 4801  brdom7disj 4804  brdom6disj 4805  unidomg 4809  alephval2 4902  alephval3 4903  cflem 4905  cflecard 4912  cfeq0 4914  cfsuc 4915  nnleltp1t 5954  lbreu 6045  lble 6047  lbinfm 6048  sup2 6051  infm3 6054  infmsup 6068  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  supxr 6081  supxrre 6083  uzwo4OLD 6210  uzwo5OLD 6211  uzwo3lem2 6217  uzwo3 6218  zmax 6220  flval2t 6238  flval3t 6239  iccsupr 6398  uzwo 6455  uzwoOLD 6456  uzinfm 6462  fsequb 6523  sqrlem6 6678  sqr2irrlem3 6726  seq1bnd 6910  cau3i 6914  cau3ir 6915  cvg1 6921  cvg3 6923  cvganz 6924  caubnd 6926  faclbnd4lem4 6951  bccl2t 6971  clim 6977  csbfsum 7027  clm3 7079  clm4 7080  clm0 7083  clm0nns 7085  clm4at 7090  climfnn 7092  climconst 7094  climshft 7104  climabs0 7113  climaddlem3 7116  climmullem8 7127  climmulc2 7129  caucvglem2 7158  caucvglem5 7161  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmp2lem 7180  cvgcmpub 7185  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  expcnvlem1 7227  expcnvlem6 7232  cncfval 7264  negfcncf 7269  elcncf1d 7270  ivthlem8 7288  efaddlem25 7362  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  infpn2 7509  ruclem33 7542  cnfval 7756  cnpfval 7757  iscn 7758  cnpval 7759  iscnp 7760  iscnp2 7761  ismet 7798  ismsg 7800  msflem 7803  opnfval 7857  metcnp2 7888  metcnpi 7890  metcnpi2 7891  metcnpi3 7892  metcnpi4 7893  metcni 7894  metcni2 7895  metcnp3 7896  metcnss 7898  cncfmet 7905  lmfval 7925  caufval 7926  lmbr 7928  lmbrf 7930  lmconst 7934  lmnn 7935  iscau 7936  iscauf 7939  iscau5 7941  iscaunns 7944  lmss 7953  causs 7955  lmclim 7963  metcnp4 7970  metcn4i 7972  xplm 7975  xpcn 7976  iscms2lem4 7992  cncms 7998  isgrp 8041  isgrpi 8042  grpideu 8053  grpidinv2 8060  cnid 8127  mulid 8132  isring 8141  ringi 8142  cnring 8162  ringsn 8163  vci 8167  isvclem 8196  isnvlem 8229  nvi 8233  nmcnilem 8337  va1cnlem 8345  sm1cnilem 8347  lnoval 8413  islno 8414  nmobndi 8438  isblo3i 8461  blo3i 8462  blocnilem 8464  blocni 8465  ajfval 8469  isphg 8476  ubthlem1 8529  ubthlem14 8542  ubthi 8544  minveclem10 8554  minveclem39 8587  htthlem7 8626  spwval2 8653  spwmo 8656  spwpr2 8658  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664  pilem2 8672  pilem3 8673  h2hcau 8849  h2hlm 8850  hilid 9028  hcau 9051  hcau2 9055  hlim 9056  hlim2 9060  hhcms 9072  sh 9078  hlim0 9105  ch2 9114  hhsscms 9150  ocelt 9154  occllem8 9180  projlem8 9193  pjth 9233  adjsymt 9759  elcnopt 9783  ellnopt 9784  elcnfnt 9809  ellnfnt 9810  cnopct 9837  cnfnct 9854  adjvalvalt 9861  0cnop 9903  0cnfn 9904  idcnop 9905  lnopeqt 9934  elunop2t 9938  lnophmt 9944  lnopcon 9963  lnopcont 9964  lnopcnbdt 9965  lnfncon 9990  lnfncont 9991  lnfncnbdt 9992  riesz3 9995  riesz4 9996  riesz4t 9997  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem4 10003  cnlnadjlem5 10004  cnlnadjlem8 10007  cnlnadj 10009  nmopadjle 10021  cnvbravalt 10043  leopg 10055  leoppost 10059  stelt 10141  mdbrt 10221  dmdbrt 10226  cdj3 10368  ghomgrpilem1 10385  homeofval 10516  ishomeo 10517  cnvhmphb 10526  cnvhmph 10527  hmeogrp 10538  hmeobc 10542  isded 10669  dedi 10670  iscat 10687  cati 10688  ismona 10737  isepia 10747  isfunb 10755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1649

Copyright terms: Public domain