Theorem rexralbidv 2392

Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexralbidv	|- ( ph -> ( E. x e. A A. y e. B ps <-> E. 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 rexralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ralbidv 2368	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2369	1 |- ( ph -> ( E. x e. A A. y e. B ps <-> E. x e. A A. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 103   A.wral 2348   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  caucvgpr  6872  caucvgprpr  6902  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  axcaucvglemres  7065  cvg1nlemres  9871  rexfiuz  9875  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  cau3lem  10000  caubnd2  10003  climi  10126  2clim  10140