Theorem 2ralbidv 2574

Description: Formula-building rule for restricted universal quantifiers (deduction form). (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 2550	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2550	1 |- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  cbvral3v  2801  poeq1  4444  soeq1  4460  isoeq1  6007  isoeq2  6008  isoeq3  6009  fnmpoovd  6451  smoeq  6561  xpf1o  7144  papeq1  7609  papcotr  7613  tapeq1  7618  elinp  7841  cauappcvgpr  8029  seq3caopr2  10932  seqcaopr2g  10933  wrd2ind  11497  addcn2  12078  mulcn2  12080  sgrp1  13728  ismhm  13770  mhmex  13771  issubm  13781  isnsg  14007  nmznsg  14018  isghm  14048  iscmn  14098  ring1  14366  opprsubrngg  14521  issubrg3  14557  islmod  14629  lmodlema  14630  lsssetm  14695  islssmd  14698  islidlm  14818  ispsmet  15426  ismet  15447  isxmet  15448  addcncntoplem  15664  elcncf  15676  mpodvdsmulf1o  16110