Metamath Proof Explorer

Theorem extid

Description: Property of identity relation, see also extep , extssr and the comment of df-ssr . (Contributed by Peter Mazsa, 5-Jul-2019)

Ref Expression
Assertion extid 
|- ( A e. V -> ( [ A ] `' _I = [ B ] `' _I <-> A = B ) )

Proof

Step Hyp Ref Expression
1 cnvi 
 |-  `' _I = _I
2 1 eceq2i 
 |-  [ A ] `' _I = [ A ] _I
3 ecidsn 
 |-  [ A ] _I = { A }
4 2 3 eqtri 
 |-  [ A ] `' _I = { A }
5 1 eceq2i 
 |-  [ B ] `' _I = [ B ] _I
6 ecidsn 
 |-  [ B ] _I = { B }
7 5 6 eqtri 
 |-  [ B ] `' _I = { B }
8 4 7 eqeq12i 
 |-  ( [ A ] `' _I = [ B ] `' _I <-> { A } = { B } )
9 sneqbg 
 |-  ( A e. V -> ( { A } = { B } <-> A = B ) )
10 8 9 bitrid 
 |-  ( A e. V -> ( [ A ] `' _I = [ B ] `' _I <-> A = B ) )