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 ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2528

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  cbvral3v  2801  poeq1  4442  soeq1  4458  isoeq1  6001  isoeq2  6002  isoeq3  6003  fnmpoovd  6445  smoeq  6555  xpf1o  7138  papeq1  7603  papcotr  7607  tapeq1  7612  elinp  7835  cauappcvgpr  8023  seq3caopr2  10913  seqcaopr2g  10914  wrd2ind  11478  addcn2  12059  mulcn2  12061  sgrp1  13709  ismhm  13751  mhmex  13752  issubm  13762  isnsg  13988  nmznsg  13999  isghm  14029  iscmn  14079  ring1  14347  opprsubrngg  14502  issubrg3  14538  islmod  14610  lmodlema  14611  lsssetm  14676  islssmd  14679  islidlm  14799  ispsmet  15407  ismet  15428  isxmet  15429  addcncntoplem  15645  elcncf  15657  mpodvdsmulf1o  16087