Theorem bm1.3ii 4784

Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4781. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
bm1.3ii.1	|- E. x A. y ( ph -> y e. x )

Assertion

Ref	Expression
bm1.3ii	|- E. x A. y ( y e. x <-> ph )

Distinct variable groups:   ph, x   x, y

Allowed substitution hint:   ph( y)

Proof of Theorem bm1.3ii

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.42v 1918	. . 3 |- ( E. x ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) <-> ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) ) )
2		bimsc1 980	. . . . 5 |- ( ( ( ph -> y e. z ) /\ ( y e. x <-> ( y e. z /\ ph ) ) ) -> ( y e. x <-> ph ) )
3	2	alanimi 1744	. . . 4 |- ( ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> A. y ( y e. x <-> ph ) )
4	3	eximi 1762	. . 3 |- ( E. x ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> E. x A. y ( y e. x <-> ph ) )
5	1, 4	sylbir 225	. 2 |- ( ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> E. x A. y ( y e. x <-> ph ) )
6		bm1.3ii.1	. . . . 5 |- E. x A. y ( ph -> y e. x )
7		elequ2 2004	. . . . . . . 8 |- ( x = z -> ( y e. x <-> y e. z ) )
8	7	imbi2d 330	. . . . . . 7 |- ( x = z -> ( ( ph -> y e. x ) <-> ( ph -> y e. z ) ) )
9	8	albidv 1849	. . . . . 6 |- ( x = z -> ( A. y ( ph -> y e. x ) <-> A. y ( ph -> y e. z ) ) )
10	9	cbvexv 2275	. . . . 5 |- ( E. x A. y ( ph -> y e. x ) <-> E. z A. y ( ph -> y e. z ) )
11	6, 10	mpbi 220	. . . 4 |- E. z A. y ( ph -> y e. z )
12		ax-sep 4781	. . . 4 |- E. x A. y ( y e. x <-> ( y e. z /\ ph ) )
13	11, 12	pm3.2i 471	. . 3 |- ( E. z A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) )
14	13	exan 1788	. 2 |- E. z ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) )
15	5, 14	exlimiiv 1859	1 |- E. x A. y ( y e. x <-> ph )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-11 2034  ax-12 2047  ax-13 2246  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  axpow3  4846  pwex  4848  zfpair2  4907  axun2  6951  uniex2  6952