Metamath Proof Explorer

Theorem sbceqal

Description: Class version of one implication of equvelv . (Contributed by Andrew Salmon, 28-Jun-2011) (Proof shortened by SN, 26-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = A -> ( x = A <-> A = A ) )
2 eqeq1 
 |-  ( x = A -> ( x = B <-> A = B ) )
3 1 2 imbi12d 
 |-  ( x = A -> ( ( x = A -> x = B ) <-> ( A = A -> A = B ) ) )
4 eqid 
 |-  A = A
5 4 a1bi 
 |-  ( A = B <-> ( A = A -> A = B ) )
6 3 5 bitr4di 
 |-  ( x = A -> ( ( x = A -> x = B ) <-> A = B ) )
7 6 spcgv 
 |-  ( A e. V -> ( A. x ( x = A -> x = B ) -> A = B ) )