Theorem 2rexbidv 2519

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2478

This theorem is referenced by:  f1oiso  5870  elrnmpog  6032  elrnmpo  6033  ralrnmpo  6034  rexrnmpo  6035  ovelrn  6069  eroveu  6682  genipv  7571  genpelxp  7573  genpelvl  7574  genpelvu  7575  axcnre  7943  apreap  8608  apreim  8624  aprcl  8667  aptap  8671  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  pythagtriplem19  12423  pceu  12436  pcval  12437  pczpre  12438  pcdiv  12443  4sqlem2  12530  4sqlem3  12531  4sqlem4  12533  4sqexercise2  12540  4sqlemsdc  12541  4sq  12551  znunit  14158  txuni2  14435  txbas  14437  txdis1cn  14457  elply  14913  2sqlem2  15272  2sqlem8  15280  2sqlem9  15281