Theorem 2ralbidv 2747

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  cbvral3v  2947  ralxpxfr2d  3073  poeq1  4631  soeq1  4647  isoeq1  5997  isoeq2  5998  isoeq3  5999  fnmpt2ovd  6640  smoeq  6797  xpf1o  7461  nqereu  9086  dedekind  9521  dedekindle  9522  seqcaopr2  11826  wrd2ind  12356  addcn2  13055  mulcn2  13057  mreexexd  14569  catlid  14604  catrid  14605  isfunc  14757  funcres2b  14790  isfull  14803  isfth  14807  fullres2c  14832  isnat  14840  evlfcl  15015  uncfcurf  15032  isprs  15083  isdrs  15087  ispos  15100  istos  15188  isdlat  15346  ismhm  15449  issubm  15457  isnsg  15690  isghm  15727  isga  15789  sylow2blem2  16100  efglem  16193  efgi  16196  efgredlemb  16223  efgred  16225  frgpuplem  16249  iscmn  16264  isirred  16725  islmod  16876  lmodlema  16877  lssset  16937  islssd  16939  islmhm  17030  islmhm2  17041  isobs  17987  mdetunilem3  18262  mdetunilem4  18263  mdetunilem9  18268  hausnei2  18799  dfcon2  18865  llyeq  18916  nllyeq  18917  isucn2  19696  iducn  19700  ispsmet  19722  ismet  19740  isxmet  19741  metucnOLD  20005  metucn  20006  ngptgp  20064  nlmvscnlem1  20109  xmetdcn2  20256  addcnlem  20282  elcncf  20307  ipcnlem1  20599  cfili  20621  c1lip1  21311  aalioulem5  21687  aalioulem6  21688  aaliou  21689  aaliou2  21691  aaliou2b  21692  ulmcau  21745  ulmdvlem3  21752  cxpcn3lem  22070  dvdsmulf1o  22419  chpdifbndlem2  22688  pntrsumbnd2  22701  istrkgb  22803  axtgsegcon  22810  axtg5seg  22811  axtgpasch  22813  axtgupdim2  22817  axtgeucl  22818  iscgrg  22846  f1otrg  22940  axcontlem10  23042  axcontlem12  23044  isgrpo  23506  isablo  23593  isass  23626  elghomlem1  23671  elghomlem2  23672  iscom2  23722  vacn  23912  smcnlem  23915  lnoval  23975  islno  23976  isphg  24040  ajmoi  24082  ajval  24085  adjmo  25059  elcnop  25084  ellnop  25085  elunop  25099  elhmop  25100  elcnfn  25109  ellnfn  25110  adjeu  25116  adjval  25117  adj1  25160  adjeq  25162  cnlnadjlem9  25302  cnlnadjeu  25305  cnlnssadj  25307  isst  25440  ishst  25441  cdj1i  25660  cdj3i  25668  resspos  25943  resstos  25944  isomnd  25988  isslmd  26067  slmdlema  26068  isorng  26120  qqhucn  26275  txpcon  26969  nofulllem4  27693  nofulllem5  27694  heicant  28270  nn0prpw  28362  equivbnd  28533  isismty  28544  heibor1lem  28552  iccbnd  28583  isrngohom  28615  pridlval  28677  ispridl  28678  isdmn3  28718  isfrgra  30428  lindslinindsimp2  30706  islfl  32278  isopos  32398  psubspset  32961  islaut  33300  ispautN  33316  ltrnset  33335  isltrn  33336  istrnN  33374  istendo  33977