Theorem sbceqalOLD

Description: Obsolete version of sbceqal as of 26-Oct-2024. (Contributed by Andrew Salmon, 28-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbceqalOLD	|- ( 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		eqsbc1	|- ( 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		eqsbc1	|- ( 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 ) )