Theorem rexralbidv 2459

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 2435	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2436	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 2414   E.wrex 2415

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420

This theorem is referenced by:  caucvgpr  7483  caucvgprpr  7513  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  axcaucvglemres  7700  cvg1nlemres  10750  rexfiuz  10754  resqrexlemgt0  10785  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemsqa  10789  resqrexlemex  10790  cau3lem  10879  caubnd2  10882  climi  11049  2clim  11063  ennnfonelemim  11926  lmcvg  12375  lmss  12404  txlm  12437  metcnpi  12673  metcnpi2  12674  elcncf  12718  cncfi  12723  limcimo  12792  cnplimclemr  12796  limccoap  12805