Theorem 2ralbidv 2887

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

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

This theorem is referenced by:  cbvral3v  3080  ralxpxfr2d  3210  poeq1  4793  soeq1  4809  isoeq1  6200  isoeq2  6201  isoeq3  6202  fnmpt2ovd  6863  smoeq  7023  xpf1o  7681  nqereu  9310  dedekind  9747  dedekindle  9748  seqcaopr2  12124  wrd2ind  12684  addcn2  13397  mulcn2  13399  mreexexd  15026  catlid  15061  catrid  15062  isfunc  15211  funcres2b  15244  isfull  15257  isfth  15261  fullres2c  15286  isnat  15294  evlfcl  15469  uncfcurf  15486  isprs  15537  isdrs  15541  ispos  15554  istos  15643  isdlat  15801  sgrp1  15896  ismhm  15946  issubm  15956  sgrp2nmndlem4  16024  isnsg  16208  isghm  16245  isga  16307  pmtrdifwrdel  16488  sylow2blem2  16619  efglem  16712  efgi  16715  efgredlemb  16742  efgred  16744  frgpuplem  16768  iscmn  16783  ring1  17226  isirred  17326  islmod  17494  lmodlema  17495  lssset  17558  islssd  17560  islmhm  17651  islmhm2  17662  isobs  18728  dmatel  18972  dmatmulcl  18979  scmateALT  18991  mdetunilem3  19093  mdetunilem4  19094  mdetunilem9  19099  cpmatel  19189  chpscmat  19320  hausnei2  19831  dfcon2  19897  llyeq  19948  nllyeq  19949  isucn2  20759  iducn  20763  ispsmet  20785  ismet  20803  isxmet  20804  metucnOLD  21068  metucn  21069  ngptgp  21127  nlmvscnlem1  21172  xmetdcn2  21319  addcnlem  21345  elcncf  21370  ipcnlem1  21662  cfili  21684  c1lip1  22375  aalioulem5  22708  aalioulem6  22709  aaliou  22710  aaliou2  22712  aaliou2b  22713  ulmcau  22766  ulmdvlem3  22773  cxpcn3lem  23097  dvdsmulf1o  23446  chpdifbndlem2  23715  pntrsumbnd2  23728  istrkgb  23828  axtgsegcon  23837  axtg5seg  23838  axtgpasch  23840  axtgupdim2  23845  axtgeucl  23846  iscgrg  23880  isismt  23897  isperp2  24068  f1otrg  24150  axcontlem10  24252  axcontlem12  24254  isfrgra  24966  isgrpo  25174  isablo  25261  isass  25294  elghomlem1OLD  25339  elghomlem2OLD  25340  iscom2  25390  vacn  25580  smcnlem  25583  lnoval  25643  islno  25644  isphg  25708  ajmoi  25750  ajval  25753  adjmo  26727  elcnop  26752  ellnop  26753  elunop  26767  elhmop  26768  elcnfn  26777  ellnfn  26778  adjeu  26784  adjval  26785  adj1  26828  adjeq  26830  cnlnadjlem9  26970  cnlnadjeu  26973  cnlnssadj  26975  isst  27108  ishst  27109  cdj1i  27328  cdj3i  27336  resspos  27624  resstos  27625  isomnd  27668  isslmd  27722  slmdlema  27723  isorng  27766  qqhucn  27950  ismntop  27981  txpcon  28654  nofulllem4  29440  nofulllem5  29441  heicant  30024  nn0prpw  30116  equivbnd  30261  isismty  30272  heibor1lem  30280  iccbnd  30311  isrngohom  30343  pridlval  30405  ispridl  30406  isdmn3  30446  ismgmhm  32309  issubmgm  32315  isrnghm  32416  lidlmsgrp  32442  lidlrng  32443  dmatALTbasel  32738  lindslinindsimp2  32799  lmod1  32828  islfl  34525  isopos  34645  psubspset  35208  islaut  35547  ispautN  35563  ltrnset  35582  isltrn  35583  istrnN  35622  istendo  36226