Metamath Proof Explorer


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 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 ) )