Theorem rexralbidv 2532

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 2506	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2507	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 2484   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  caucvgpr  7797  caucvgprpr  7827  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  axcaucvglemres  8014  cvg1nlemres  11329  rexfiuz  11333  resqrexlemgt0  11364  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  cau3lem  11458  caubnd2  11461  climi  11631  2clim  11645  ennnfonelemim  12828  mplelbascoe  14487  lmcvg  14722  lmss  14751  txlm  14784  metcnpi  15020  metcnpi2  15021  elcncf  15078  cncfi  15083  limcimo  15170  cnplimclemr  15174  limccoap  15183