Theorem 2ralbidv 2844

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 2839	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2839	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 189   A.wral 2749

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

This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2754

This theorem is referenced by:  cbvral3v  3041  ralxpxfr2d  3176  poeq1  4777  soeq1  4793  isoeq1  6235  isoeq2  6236  isoeq3  6237  fnmpt2ovd  6898  smoeq  7095  xpf1o  7760  nqereu  9380  dedekind  9823  dedekindle  9824  seqcaopr2  12281  wrd2ind  12871  addcn2  13706  mulcn2  13708  mreexexd  15603  catlid  15638  catrid  15639  isfunc  15818  funcres2b  15851  isfull  15864  isfth  15868  fullres2c  15893  isnat  15901  evlfcl  16156  uncfcurf  16173  isprs  16224  isdrs  16228  ispos  16241  istos  16330  isdlat  16488  sgrp1  16583  ismhm  16633  issubm  16643  sgrp2nmndlem4  16711  isnsg  16895  isghm  16932  isga  16994  pmtrdifwrdel  17175  sylow2blem2  17322  efglem  17415  efgi  17418  efgredlemb  17445  efgred  17447  frgpuplem  17471  iscmn  17486  ring1  17879  isirred  17976  islmod  18144  lmodlema  18145  lssset  18206  islssd  18208  islmhm  18299  islmhm2  18310  isobs  19332  dmatel  19567  dmatmulcl  19574  scmateALT  19586  mdetunilem3  19688  mdetunilem4  19689  mdetunilem9  19694  cpmatel  19784  chpscmat  19915  hausnei2  20418  dfcon2  20483  llyeq  20534  nllyeq  20535  isucn2  21343  iducn  21347  ispsmet  21369  ismet  21387  isxmet  21388  metucn  21635  ngptgp  21693  nlmvscnlem1  21738  xmetdcn2  21904  addcnlem  21945  elcncf  21970  ipcnlem1  22265  cfili  22287  c1lip1  22998  aalioulem5  23341  aalioulem6  23342  aaliou  23343  aaliou2  23345  aaliou2b  23346  ulmcau  23399  ulmdvlem3  23406  cxpcn3lem  23736  dvdsmulf1o  24172  chpdifbndlem2  24441  pntrsumbnd2  24454  istrkgb  24552  axtgsegcon  24561  axtg5seg  24562  axtgpasch  24564  axtgeucl  24569  iscgrg  24606  isismt  24628  isperp2  24809  f1otrg  24950  axcontlem10  25052  axcontlem12  25054  isfrgra  25767  isgrpo  25973  isablo  26060  isass  26093  elghomlem1OLD  26138  elghomlem2OLD  26139  iscom2  26189  vacn  26379  smcnlem  26382  lnoval  26442  islno  26443  isphg  26507  ajmoi  26549  ajval  26552  adjmo  27534  elcnop  27559  ellnop  27560  elunop  27574  elhmop  27575  elcnfn  27584  ellnfn  27585  adjeu  27591  adjval  27592  adj1  27635  adjeq  27637  cnlnadjlem9  27777  cnlnadjeu  27780  cnlnssadj  27782  isst  27915  ishst  27916  cdj1i  28135  cdj3i  28143  resspos  28469  resstos  28470  isomnd  28513  isslmd  28567  slmdlema  28568  isorng  28611  qqhucn  28845  ismntop  28879  axtgupdim2OLD  29534  txpcon  30004  nofulllem4  30643  nofulllem5  30644  nn0prpw  31028  heicant  32020  equivbnd  32167  isismty  32178  heibor1lem  32186  iccbnd  32217  isrngohom  32249  pridlval  32311  ispridl  32312  isdmn3  32352  islfl  32671  isopos  32791  psubspset  33354  islaut  33693  ispautN  33709  ltrnset  33728  isltrn  33729  istrnN  33768  istendo  34372  ismgmhm  40056  issubmgm  40062  isrnghm  40165  lidlmsgrp  40199  lidlrng  40200  dmatALTbasel  40468  lindslinindsimp2  40529  lmod1  40558