Theorem rexralbidv 2503

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 2477	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2478	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 2455   E.wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  caucvgpr  7683  caucvgprpr  7713  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  axcaucvglemres  7900  cvg1nlemres  10996  rexfiuz  11000  resqrexlemgt0  11031  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  cau3lem  11125  caubnd2  11128  climi  11297  2clim  11311  ennnfonelemim  12427  lmcvg  13802  lmss  13831  txlm  13864  metcnpi  14100  metcnpi2  14101  elcncf  14145  cncfi  14150  limcimo  14219  cnplimclemr  14223  limccoap  14232