Theorem bm1.3ii

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

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

Proof

Step	Hyp	Ref	Expression
1		bm1.3ii.1	|- E. x A. y ( ph -> y e. x )
2		19.42v	|- ( 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 ) ) ) )
3		bimsc1	|- ( ( ( ph -> y e. z ) /\ ( y e. x <-> ( y e. z /\ ph ) ) ) -> ( y e. x <-> ph ) )
4	3	alanimi	|- ( ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> A. y ( y e. x <-> ph ) )
5	4	eximi	|- ( 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 ) )
6	2 5	sylbir	|- ( ( 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 ) )
7		elequ2	|- ( x = z -> ( y e. x <-> y e. z ) )
8	7	imbi2d	|- ( x = z -> ( ( ph -> y e. x ) <-> ( ph -> y e. z ) ) )
9	8	albidv	|- ( x = z -> ( A. y ( ph -> y e. x ) <-> A. y ( ph -> y e. z ) ) )
10	9	cbvexvw	|- ( E. x A. y ( ph -> y e. x ) <-> E. z A. y ( ph -> y e. z ) )
11	1 10	mpbi	|- E. z A. y ( ph -> y e. z )
12		ax-sep	|- E. x A. y ( y e. x <-> ( y e. z /\ ph ) )
13	11 12	exan	|- E. z ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) )
14	6 13	exlimiiv	|- E. x A. y ( y e. x <-> ph )