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  4446  soeq1  4462  isoeq1  6010  isoeq2  6011  isoeq3  6012  fnmpoovd  6455  smoeq  6566  xpf1o  7150  papeq1  7616  papcotr  7620  tapeq1  7625  elinp  7848  cauappcvgpr  8036  seq3caopr2  10951  seqcaopr2g  10952  wrd2ind  11517  addcn2  12101  mulcn2  12103  sgrp1  13785  ismhm  13827  mhmex  13828  issubm  13838  isnsg  14064  nmznsg  14075  isghm  14105  iscmn  14186  ring1  14471  opprsubrngg  14628  issubrg3  14664  islmod  14736  lmodlema  14737  lsssetm  14802  islssmd  14805  islidlm  14925  ispsmet  15582  ismet  15603  isxmet  15604  addcncntoplem  15820  elcncf  15832  mpodvdsmulf1o  16317