Theorem 2ralbidv 2908

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 2903	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2903	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 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819

This theorem is referenced by:  cbvral3v  3098  ralxpxfr2d  3228  poeq1  4803  soeq1  4819  isoeq1  6203  isoeq2  6204  isoeq3  6205  fnmpt2ovd  6861  smoeq  7021  xpf1o  7679  nqereu  9307  dedekind  9743  dedekindle  9744  seqcaopr2  12111  wrd2ind  12666  addcn2  13379  mulcn2  13381  mreexexd  14903  catlid  14938  catrid  14939  isfunc  15091  funcres2b  15124  isfull  15137  isfth  15141  fullres2c  15166  isnat  15174  evlfcl  15349  uncfcurf  15366  isprs  15417  isdrs  15421  ispos  15434  istos  15522  isdlat  15680  ismhm  15788  issubm  15797  isnsg  16035  isghm  16072  isga  16134  sylow2blem2  16447  efglem  16540  efgi  16543  efgredlemb  16570  efgred  16572  frgpuplem  16596  iscmn  16611  isirred  17149  islmod  17316  lmodlema  17317  lssset  17380  islssd  17382  islmhm  17473  islmhm2  17484  isobs  18546  dmatel  18790  scmateALT  18809  mdetunilem3  18911  mdetunilem4  18912  mdetunilem9  18917  chpscmat  19138  hausnei2  19648  dfcon2  19714  llyeq  19765  nllyeq  19766  isucn2  20545  iducn  20549  ispsmet  20571  ismet  20589  isxmet  20590  metucnOLD  20854  metucn  20855  ngptgp  20913  nlmvscnlem1  20958  xmetdcn2  21105  addcnlem  21131  elcncf  21156  ipcnlem1  21448  cfili  21470  c1lip1  22161  aalioulem5  22494  aalioulem6  22495  aaliou  22496  aaliou2  22498  aaliou2b  22499  ulmcau  22552  ulmdvlem3  22559  cxpcn3lem  22877  dvdsmulf1o  23226  chpdifbndlem2  23495  pntrsumbnd2  23508  istrkgb  23608  axtgsegcon  23617  axtg5seg  23618  axtgpasch  23620  axtgupdim2  23625  axtgeucl  23626  iscgrg  23660  isperp2  23828  f1otrg  23878  axcontlem10  23980  axcontlem12  23982  isfrgra  24694  isgrpo  24902  isablo  24989  isass  25022  elghomlem1  25067  elghomlem2  25068  iscom2  25118  vacn  25308  smcnlem  25311  lnoval  25371  islno  25372  isphg  25436  ajmoi  25478  ajval  25481  adjmo  26455  elcnop  26480  ellnop  26481  elunop  26495  elhmop  26496  elcnfn  26505  ellnfn  26506  adjeu  26512  adjval  26513  adj1  26556  adjeq  26558  cnlnadjlem9  26698  cnlnadjeu  26701  cnlnssadj  26703  isst  26836  ishst  26837  cdj1i  27056  cdj3i  27064  resspos  27337  resstos  27338  isomnd  27381  isslmd  27435  slmdlema  27436  isorng  27480  qqhucn  27637  txpcon  28345  nofulllem4  29070  nofulllem5  29071  heicant  29654  nn0prpw  29746  equivbnd  29917  isismty  29928  heibor1lem  29936  iccbnd  29967  isrngohom  29999  pridlval  30061  ispridl  30062  isdmn3  30102  dmatALTbasel  32102  lindslinindsimp2  32163  islfl  33875  isopos  33995  psubspset  34558  islaut  34897  ispautN  34913  ltrnset  34932  isltrn  34933  istrnN  34971  istendo  35574