Theorem 2rexbidv 2531

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 2507	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2507	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 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-rex 2490

This theorem is referenced by:  f1oiso  5897  elrnmpog  6060  elrnmpo  6061  ralrnmpo  6062  rexrnmpo  6063  ovelrn  6097  eroveu  6715  genipv  7624  genpelxp  7626  genpelvl  7627  genpelvu  7628  axcnre  7996  apreap  8662  apreim  8678  aprcl  8721  aptap  8725  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  pythagtriplem19  12638  pceu  12651  pcval  12652  pczpre  12653  pcdiv  12658  4sqlem2  12745  4sqlem3  12746  4sqlem4  12748  4sqexercise2  12755  4sqlemsdc  12756  4sq  12766  znunit  14454  txuni2  14761  txbas  14763  txdis1cn  14783  elply  15239  2sqlem2  15625  2sqlem8  15633  2sqlem9  15634