Theorem rexralbidv 2558

Description: Formula-building rule for restricted quantifiers (deduction form). (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 2532	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2533	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 105   A.wral 2510   E.wrex 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  caucvgpr  7902  caucvgprpr  7932  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  axcaucvglemres  8119  cvg1nlemres  11547  rexfiuz  11551  resqrexlemgt0  11582  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemsqa  11586  resqrexlemex  11587  cau3lem  11676  caubnd2  11679  climi  11849  2clim  11863  ennnfonelemim  13047  mplelbascoe  14709  lmcvg  14944  lmss  14973  txlm  15006  metcnpi  15242  metcnpi2  15243  elcncf  15300  cncfi  15305  limcimo  15392  cnplimclemr  15396  limccoap  15405