Theorem sbceqal

Description: Class version of one implication of equvelv . (Contributed by Andrew Salmon, 28-Jun-2011)

	Ref	Expression
Assertion	sbceqal	|- ( A e. V -> ( A. x ( x = A -> x = B ) -> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		spsbc	|- ( A e. V -> ( A. x ( x = A -> x = B ) -> [. A / x ]. ( x = A -> x = B ) ) )
2		sbcimg	|- ( A e. V -> ( [. A / x ]. ( x = A -> x = B ) <-> ( [. A / x ]. x = A -> [. A / x ]. x = B ) ) )
3		eqid	|- A = A
4		eqsbc3	|- ( A e. V -> ( [. A / x ]. x = A <-> A = A ) )
5	3 4	mpbiri	|- ( A e. V -> [. A / x ]. x = A )
6		pm5.5	|- ( [. A / x ]. x = A -> ( ( [. A / x ]. x = A -> [. A / x ]. x = B ) <-> [. A / x ]. x = B ) )
7	5 6	syl	|- ( A e. V -> ( ( [. A / x ]. x = A -> [. A / x ]. x = B ) <-> [. A / x ]. x = B ) )
8		eqsbc3	|- ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )
9	2 7 8	3bitrd	|- ( A e. V -> ( [. A / x ]. ( x = A -> x = B ) <-> A = B ) )
10	1 9	sylibd	|- ( A e. V -> ( A. x ( x = A -> x = B ) -> A = B ) )