Theorem 2ralbidv 2708

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 2686	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2686	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 177   A.wral 2666

This theorem is referenced by:  cbvral3v  2902  poeq1  4466  soeq1  4482  isoeq1  5998  isoeq2  5999  isoeq3  6000  smoeq  6571  xpf1o  7228  nqereu  8762  seqcaopr2  11314  addcn2  12342  mulcn2  12344  mreexexd  13828  catlid  13863  catrid  13864  isfunc  14016  funcres2b  14049  isfull  14062  isfth  14066  fullres2c  14091  isnat  14099  evlfcl  14274  uncfcurf  14291  isprs  14342  isdrs  14346  ispos  14359  istos  14419  islat  14431  isdlat  14574  ismhm  14695  issubm  14703  isnsg  14924  isghm  14961  isga  15023  sylow2blem2  15210  efglem  15303  efgi  15306  efgredlemb  15333  efgred  15335  frgpuplem  15359  iscmn  15374  isirred  15759  islmod  15909  lmodlema  15910  lssset  15965  islssd  15967  islmhm  16058  islmhm2  16069  isobs  16902  hausnei2  17371  dfcon2  17435  llyeq  17486  nllyeq  17487  isucn2  18262  iducn  18266  ispsmet  18288  ismet  18306  isxmet  18307  metucnOLD  18571  metucn  18572  ngptgp  18630  nlmvscnlem1  18675  xmetdcn2  18821  addcnlem  18847  elcncf  18872  ipcnlem1  19152  cfili  19174  c1lip1  19834  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou2  20210  aaliou2b  20211  ulmcau  20264  ulmdvlem3  20271  cxpcn3lem  20584  dvdsmulf1o  20932  chpdifbndlem2  21201  pntrsumbnd2  21214  isgrpo  21737  isablo  21824  isass  21857  elghomlem1  21902  elghomlem2  21903  iscom2  21953  vacn  22143  smcnlem  22146  lnoval  22206  islno  22207  isphg  22271  ajmoi  22313  ajval  22316  adjmo  23288  elcnop  23313  ellnop  23314  elunop  23328  elhmop  23329  elcnfn  23338  ellnfn  23339  adjeu  23345  adjval  23346  adj1  23389  adjeq  23391  cnlnadjlem9  23531  cnlnadjeu  23534  cnlnssadj  23536  isst  23669  ishst  23670  cdj1i  23889  cdj3i  23897  resspos  24140  resstos  24141  isofld  24188  qqhucn  24329  txpcon  24872  dedekind  25140  dedekindle  25141  nofulllem4  25573  nofulllem5  25574  axcontlem10  25816  axcontlem12  25818  nn0prpw  26216  equivbnd  26389  isismty  26400  heibor1lem  26408  iccbnd  26439  isrngohom  26471  pridlval  26533  ispridl  26534  isdmn3  26574  ralxpxfr2d  26631  isfrgra  28094  islfl  29543  isopos  29663  psubspset  30226  islaut  30565  ispautN  30581  ltrnset  30600  isltrn  30601  istrnN  30639  istendo  31242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671