Theorem rexralbidv 2496

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 2470	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2471	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 104   A.wral 2448   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  caucvgpr  7644  caucvgprpr  7674  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  axcaucvglemres  7861  cvg1nlemres  10949  rexfiuz  10953  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  cau3lem  11078  caubnd2  11081  climi  11250  2clim  11264  ennnfonelemim  12379  lmcvg  13011  lmss  13040  txlm  13073  metcnpi  13309  metcnpi2  13310  elcncf  13354  cncfi  13359  limcimo  13428  cnplimclemr  13432  limccoap  13441