Theorem 2ralbidv 2557

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  cbvral3v  2783  poeq1  4402  soeq1  4418  isoeq1  5952  isoeq2  5953  isoeq3  5954  fnmpoovd  6389  smoeq  6499  xpf1o  7073  tapeq1  7514  elinp  7737  cauappcvgpr  7925  seq3caopr2  10799  seqcaopr2g  10800  wrd2ind  11351  addcn2  11931  mulcn2  11933  sgrp1  13555  ismhm  13605  mhmex  13606  issubm  13616  isnsg  13850  nmznsg  13861  isghm  13891  iscmn  13941  ring1  14134  opprsubrngg  14287  issubrg3  14323  islmod  14367  lmodlema  14368  lsssetm  14432  islssmd  14435  islidlm  14555  ispsmet  15114  ismet  15135  isxmet  15136  addcncntoplem  15352  elcncf  15364  mpodvdsmulf1o  15784