Theorem 2rexbidv 2502

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
2rexbidv	|- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. 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 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	rexbidv 2478	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2478	1 |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 105   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-rex 2461

This theorem is referenced by:  f1oiso  5826  elrnmpog  5986  elrnmpo  5987  ralrnmpo  5988  rexrnmpo  5989  ovelrn  6022  eroveu  6625  genipv  7507  genpelxp  7509  genpelvl  7510  genpelvu  7511  axcnre  7879  apreap  8543  apreim  8559  aprcl  8602  aptap  8606  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  pythagtriplem19  12281  pceu  12294  pcval  12295  pczpre  12296  pcdiv  12301  4sqlem2  12386  4sqlem3  12387  4sqlem4  12389  txuni2  13726  txbas  13728  txdis1cn  13748  2sqlem2  14432  2sqlem8  14440  2sqlem9  14441