Theorem 2rexbidv 2555

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  f1oiso  5956  elrnmpog  6123  elrnmpo  6124  ralrnmpo  6125  rexrnmpo  6126  ovelrn  6160  eroveu  6781  genipv  7707  genpelxp  7709  genpelvl  7710  genpelvu  7711  axcnre  8079  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  pythagtriplem19  12821  pceu  12834  pcval  12835  pczpre  12836  pcdiv  12841  4sqlem2  12928  4sqlem3  12929  4sqlem4  12931  4sqexercise2  12938  4sqlemsdc  12939  4sq  12949  znunit  14639  txuni2  14946  txbas  14948  txdis1cn  14968  elply  15424  2sqlem2  15810  2sqlem8  15818  2sqlem9  15819  upgredg  15958  3dom  16439