Theorem 2ralbidv 2869

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 2864	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2864	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 187   A.wral 2775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2780

This theorem is referenced by:  cbvral3v  3065  ralxpxfr2d  3196  poeq1  4773  soeq1  4789  isoeq1  6221  isoeq2  6222  isoeq3  6223  fnmpt2ovd  6881  smoeq  7073  xpf1o  7736  nqereu  9354  dedekind  9797  dedekindle  9798  seqcaopr2  12248  wrd2ind  12824  addcn2  13644  mulcn2  13646  mreexexd  15541  catlid  15576  catrid  15577  isfunc  15756  funcres2b  15789  isfull  15802  isfth  15806  fullres2c  15831  isnat  15839  evlfcl  16094  uncfcurf  16111  isprs  16162  isdrs  16166  ispos  16179  istos  16268  isdlat  16426  sgrp1  16521  ismhm  16571  issubm  16581  sgrp2nmndlem4  16649  isnsg  16833  isghm  16870  isga  16932  pmtrdifwrdel  17113  sylow2blem2  17260  efglem  17353  efgi  17356  efgredlemb  17383  efgred  17385  frgpuplem  17409  iscmn  17424  ring1  17817  isirred  17914  islmod  18082  lmodlema  18083  lssset  18144  islssd  18146  islmhm  18237  islmhm2  18248  isobs  19269  dmatel  19504  dmatmulcl  19511  scmateALT  19523  mdetunilem3  19625  mdetunilem4  19626  mdetunilem9  19631  cpmatel  19721  chpscmat  19852  hausnei2  20355  dfcon2  20420  llyeq  20471  nllyeq  20472  isucn2  21280  iducn  21284  ispsmet  21306  ismet  21324  isxmet  21325  metucn  21572  ngptgp  21630  nlmvscnlem1  21675  xmetdcn2  21841  addcnlem  21882  elcncf  21907  ipcnlem1  22202  cfili  22224  c1lip1  22935  aalioulem5  23278  aalioulem6  23279  aaliou  23280  aaliou2  23282  aaliou2b  23283  ulmcau  23336  ulmdvlem3  23343  cxpcn3lem  23673  dvdsmulf1o  24109  chpdifbndlem2  24378  pntrsumbnd2  24391  istrkgb  24489  axtgsegcon  24498  axtg5seg  24499  axtgpasch  24501  axtgeucl  24506  iscgrg  24543  isismt  24565  isperp2  24746  f1otrg  24887  axcontlem10  24989  axcontlem12  24991  isfrgra  25703  isgrpo  25909  isablo  25996  isass  26029  elghomlem1OLD  26074  elghomlem2OLD  26075  iscom2  26125  vacn  26315  smcnlem  26318  lnoval  26378  islno  26379  isphg  26443  ajmoi  26485  ajval  26488  adjmo  27470  elcnop  27495  ellnop  27496  elunop  27510  elhmop  27511  elcnfn  27520  ellnfn  27521  adjeu  27527  adjval  27528  adj1  27571  adjeq  27573  cnlnadjlem9  27713  cnlnadjeu  27716  cnlnssadj  27718  isst  27851  ishst  27852  cdj1i  28071  cdj3i  28079  resspos  28414  resstos  28415  isomnd  28458  isslmd  28512  slmdlema  28513  isorng  28557  qqhucn  28791  ismntop  28825  axtgupdim2OLD  29480  txpcon  29950  nofulllem4  30586  nofulllem5  30587  nn0prpw  30971  heicant  31888  equivbnd  32035  isismty  32046  heibor1lem  32054  iccbnd  32085  isrngohom  32117  pridlval  32179  ispridl  32180  isdmn3  32220  islfl  32544  isopos  32664  psubspset  33227  islaut  33566  ispautN  33582  ltrnset  33601  isltrn  33602  istrnN  33641  istendo  34245  ismgmhm  39054  issubmgm  39060  isrnghm  39163  lidlmsgrp  39197  lidlrng  39198  dmatALTbasel  39468  lindslinindsimp2  39529  lmod1  39558