Theorem sbc5ALT

Description: Alternate proof of sbc5 . This proof helps show how clelab works, since it is equivalent but shorter thanks to now-available library theorems like vtoclbg and isset . (Contributed by NM, 23-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / x ]. ph -> A e. _V )
2		exsimpl	|- ( E. x ( x = A /\ ph ) -> E. x x = A )
3		isset	|- ( A e. _V <-> E. x x = A )
4	2 3	sylibr	|- ( E. x ( x = A /\ ph ) -> A e. _V )
5		dfsbcq2	|- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
6		eqeq2	|- ( y = A -> ( x = y <-> x = A ) )
7	6	anbi1d	|- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
8	7	exbidv	|- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
9		sb5	|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
10	5 8 9	vtoclbg	|- ( A e. _V -> ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) )
11	1 4 10	pm5.21nii	|- ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )