Theorem sb5ALT

Description: Equivalence for substitution. Alternate proof of sb5 . This proof is sb5ALTVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sb5ALT	|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		equsb1	|- [ y / x ] x = y
2		sban	|- ( [ y / x ] ( x = y /\ ph ) <-> ( [ y / x ] x = y /\ [ y / x ] ph ) )
3	2	simplbi2com	|- ( [ y / x ] ph -> ( [ y / x ] x = y -> [ y / x ] ( x = y /\ ph ) ) )
4	1 3	mpi	|- ( [ y / x ] ph -> [ y / x ] ( x = y /\ ph ) )
5		spsbe	|- ( [ y / x ] ( x = y /\ ph ) -> E. x ( x = y /\ ph ) )
6	4 5	syl	|- ( [ y / x ] ph -> E. x ( x = y /\ ph ) )
7		hbs1	|- ( [ y / x ] ph -> A. x [ y / x ] ph )
8		simpr	|- ( ( x = y /\ ph ) -> ph )
9	8	a1i	|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> ph ) )
10		simpl	|- ( ( x = y /\ ph ) -> x = y )
11	10	a1i	|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> x = y ) )
12		sbequ1	|- ( x = y -> ( ph -> [ y / x ] ph ) )
13	12	com12	|- ( ph -> ( x = y -> [ y / x ] ph ) )
14	9 11 13	syl6c	|- ( E. x ( x = y /\ ph ) -> ( ( x = y /\ ph ) -> [ y / x ] ph ) )
15	7 14	exlimexi	|- ( E. x ( x = y /\ ph ) -> [ y / x ] ph )
16	6 15	impbii	|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )