Theorem 2ralbidv 2532

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  cbvral3v  2757  poeq1  4364  soeq1  4380  isoeq1  5893  isoeq2  5894  isoeq3  5895  fnmpoovd  6324  smoeq  6399  xpf1o  6966  tapeq1  7399  elinp  7622  cauappcvgpr  7810  seq3caopr2  10675  seqcaopr2g  10676  wrd2ind  11214  addcn2  11736  mulcn2  11738  sgrp1  13358  ismhm  13408  mhmex  13409  issubm  13419  isnsg  13653  nmznsg  13664  isghm  13694  iscmn  13744  ring1  13936  opprsubrngg  14088  issubrg3  14124  islmod  14168  lmodlema  14169  lsssetm  14233  islssmd  14236  islidlm  14356  ispsmet  14910  ismet  14931  isxmet  14932  addcncntoplem  15148  elcncf  15160  mpodvdsmulf1o  15577