Theorem rexralbidv 2492

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 2466	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	rexbidv 2467	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 2444   E.wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  caucvgpr  7623  caucvgprpr  7653  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  axcaucvglemres  7840  cvg1nlemres  10927  rexfiuz  10931  resqrexlemgt0  10962  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemsqa  10966  resqrexlemex  10967  cau3lem  11056  caubnd2  11059  climi  11228  2clim  11242  ennnfonelemim  12357  lmcvg  12857  lmss  12886  txlm  12919  metcnpi  13155  metcnpi2  13156  elcncf  13200  cncfi  13205  limcimo  13274  cnplimclemr  13278  limccoap  13287