Theorem 2ralbidv 2778

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

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

This theorem is referenced by:  cbvral3v  2978  ralxpxfr2d  3105  poeq1  4665  soeq1  4681  isoeq1  6031  isoeq2  6032  isoeq3  6033  fnmpt2ovd  6672  smoeq  6832  xpf1o  7494  nqereu  9119  dedekind  9554  dedekindle  9555  seqcaopr2  11863  wrd2ind  12393  addcn2  13092  mulcn2  13094  mreexexd  14607  catlid  14642  catrid  14643  isfunc  14795  funcres2b  14828  isfull  14841  isfth  14845  fullres2c  14870  isnat  14878  evlfcl  15053  uncfcurf  15070  isprs  15121  isdrs  15125  ispos  15138  istos  15226  isdlat  15384  ismhm  15487  issubm  15496  isnsg  15731  isghm  15768  isga  15830  sylow2blem2  16141  efglem  16234  efgi  16237  efgredlemb  16264  efgred  16266  frgpuplem  16290  iscmn  16305  isirred  16813  islmod  16974  lmodlema  16975  lssset  17037  islssd  17039  islmhm  17130  islmhm2  17141  isobs  18167  mdetunilem3  18442  mdetunilem4  18443  mdetunilem9  18448  hausnei2  18979  dfcon2  19045  llyeq  19096  nllyeq  19097  isucn2  19876  iducn  19880  ispsmet  19902  ismet  19920  isxmet  19921  metucnOLD  20185  metucn  20186  ngptgp  20244  nlmvscnlem1  20289  xmetdcn2  20436  addcnlem  20462  elcncf  20487  ipcnlem1  20779  cfili  20801  c1lip1  21491  aalioulem5  21824  aalioulem6  21825  aaliou  21826  aaliou2  21828  aaliou2b  21829  ulmcau  21882  ulmdvlem3  21889  cxpcn3lem  22207  dvdsmulf1o  22556  chpdifbndlem2  22825  pntrsumbnd2  22838  istrkgb  22940  axtgsegcon  22947  axtg5seg  22948  axtgpasch  22950  axtgupdim2  22954  axtgeucl  22955  iscgrg  22987  isperp2  23128  f1otrg  23139  axcontlem10  23241  axcontlem12  23243  isgrpo  23705  isablo  23792  isass  23825  elghomlem1  23870  elghomlem2  23871  iscom2  23921  vacn  24111  smcnlem  24114  lnoval  24174  islno  24175  isphg  24239  ajmoi  24281  ajval  24284  adjmo  25258  elcnop  25283  ellnop  25284  elunop  25298  elhmop  25299  elcnfn  25308  ellnfn  25309  adjeu  25315  adjval  25316  adj1  25359  adjeq  25361  cnlnadjlem9  25501  cnlnadjeu  25504  cnlnssadj  25506  isst  25639  ishst  25640  cdj1i  25859  cdj3i  25867  resspos  26142  resstos  26143  isomnd  26186  isslmd  26240  slmdlema  26241  isorng  26289  qqhucn  26443  txpcon  27143  nofulllem4  27868  nofulllem5  27869  heicant  28452  nn0prpw  28544  equivbnd  28715  isismty  28726  heibor1lem  28734  iccbnd  28765  isrngohom  28797  pridlval  28859  ispridl  28860  isdmn3  28900  isfrgra  30608  dmatid  30913  scmatid  30921  scmatsubcl  30923  lindslinindsimp2  30994  islfl  32801  isopos  32921  psubspset  33484  islaut  33823  ispautN  33839  ltrnset  33858  isltrn  33859  istrnN  33897  istendo  34500