Theorem 2ralbidv 2898

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)   A( x, y)   B( x, y)

Proof of Theorem 2ralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ralbidv 2893	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2893	1 |- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wral 2804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2809

This theorem is referenced by:  cbvral3v  3091  ralxpxfr2d  3221  poeq1  4792  soeq1  4808  isoeq1  6190  isoeq2  6191  isoeq3  6192  fnmpt2ovd  6851  smoeq  7013  xpf1o  7672  nqereu  9296  dedekind  9733  dedekindle  9734  seqcaopr2  12128  wrd2ind  12697  addcn2  13501  mulcn2  13503  mreexexd  15140  catlid  15175  catrid  15176  isfunc  15355  funcres2b  15388  isfull  15401  isfth  15405  fullres2c  15430  isnat  15438  evlfcl  15693  uncfcurf  15710  isprs  15761  isdrs  15765  ispos  15778  istos  15867  isdlat  16025  sgrp1  16120  ismhm  16170  issubm  16180  sgrp2nmndlem4  16248  isnsg  16432  isghm  16469  isga  16531  pmtrdifwrdel  16712  sylow2blem2  16843  efglem  16936  efgi  16939  efgredlemb  16966  efgred  16968  frgpuplem  16992  iscmn  17007  ring1  17446  isirred  17546  islmod  17714  lmodlema  17715  lssset  17778  islssd  17780  islmhm  17871  islmhm2  17882  isobs  18927  dmatel  19165  dmatmulcl  19172  scmateALT  19184  mdetunilem3  19286  mdetunilem4  19287  mdetunilem9  19292  cpmatel  19382  chpscmat  19513  hausnei2  20024  dfcon2  20089  llyeq  20140  nllyeq  20141  isucn2  20951  iducn  20955  ispsmet  20977  ismet  20995  isxmet  20996  metucnOLD  21260  metucn  21261  ngptgp  21319  nlmvscnlem1  21364  xmetdcn2  21511  addcnlem  21537  elcncf  21562  ipcnlem1  21854  cfili  21876  c1lip1  22567  aalioulem5  22901  aalioulem6  22902  aaliou  22903  aaliou2  22905  aaliou2b  22906  ulmcau  22959  ulmdvlem3  22966  cxpcn3lem  23292  dvdsmulf1o  23671  chpdifbndlem2  23940  pntrsumbnd2  23953  istrkgb  24053  axtgsegcon  24062  axtg5seg  24063  axtgpasch  24065  axtgupdim2  24070  axtgeucl  24071  iscgrg  24108  isismt  24125  isperp2  24296  f1otrg  24379  axcontlem10  24481  axcontlem12  24483  isfrgra  25195  isgrpo  25399  isablo  25486  isass  25519  elghomlem1OLD  25564  elghomlem2OLD  25565  iscom2  25615  vacn  25805  smcnlem  25808  lnoval  25868  islno  25869  isphg  25933  ajmoi  25975  ajval  25978  adjmo  26952  elcnop  26977  ellnop  26978  elunop  26992  elhmop  26993  elcnfn  27002  ellnfn  27003  adjeu  27009  adjval  27010  adj1  27053  adjeq  27055  cnlnadjlem9  27195  cnlnadjeu  27198  cnlnssadj  27200  isst  27333  ishst  27334  cdj1i  27553  cdj3i  27561  resspos  27884  resstos  27885  isomnd  27928  isslmd  27982  slmdlema  27983  isorng  28027  qqhucn  28210  ismntop  28241  txpcon  28944  nofulllem4  29708  nofulllem5  29709  heicant  30292  nn0prpw  30384  equivbnd  30529  isismty  30540  heibor1lem  30548  iccbnd  30579  isrngohom  30611  pridlval  30673  ispridl  30674  isdmn3  30714  ismgmhm  32862  issubmgm  32868  isrnghm  32971  lidlmsgrp  33005  lidlrng  33006  dmatALTbasel  33276  lindslinindsimp2  33337  lmod1  33366  islfl  35201  isopos  35321  psubspset  35884  islaut  36223  ispautN  36239  ltrnset  36258  isltrn  36259  istrnN  36298  istendo  36902