Metamath Proof Explorer

Theorem bj-ideqb

Description: Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023)

Ref Expression
Assertion bj-ideqb 
|- ( A _I B <-> ( A e. _V /\ A = B ) )

Proof

Step Hyp Ref Expression
1 reli 
 |-  Rel _I
2 1 brrelex1i 
 |-  ( A _I B -> A e. _V )
3 inex1g 
 |-  ( A e. _V -> ( A i^i B ) e. _V )
4 bj-ideqg 
 |-  ( ( A i^i B ) e. _V -> ( A _I B <-> A = B ) )
5 3 4 syl 
 |-  ( A e. _V -> ( A _I B <-> A = B ) )
6 2 5 biadanii 
 |-  ( A _I B <-> ( A e. _V /\ A = B ) )