Theorem rexralbidv 2433

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 2409	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2410	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 2388   E.wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-ral 2393  df-rex 2394

This theorem is referenced by:  caucvgpr  7432  caucvgprpr  7462  caucvgsrlemgt1  7531  caucvgsrlemoffres  7536  axcaucvglemres  7628  cvg1nlemres  10643  rexfiuz  10647  resqrexlemgt0  10678  resqrexlemoverl  10679  resqrexlemglsq  10680  resqrexlemsqa  10682  resqrexlemex  10683  cau3lem  10772  caubnd2  10775  climi  10942  2clim  10956  ennnfonelemim  11776  lmcvg  12222  lmss  12251  txlm  12284  metcnpi  12498  metcnpi2  12499  elcncf  12540  cncfi  12545  limcimo  12584  cnplimclemr  12588