Metamath Proof Explorer

Theorem bj-opelid

Description: Characterization of the ordered pair elements of the identity relation when the intersection of their components are sets. Note that the antecedent is more general than either component being a set. (Contributed by BJ, 29-Mar-2020)

Ref Expression
Assertion bj-opelid 
|- ( ( A i^i B ) e. V -> ( <. A , B >. e. _I <-> A = B ) )

Proof

Step Hyp Ref Expression
1 bj-inexeqex 
 |-  ( ( ( A i^i B ) e. V /\ A = B ) -> ( A e. _V /\ B e. _V ) )
2 1 ex 
 |-  ( ( A i^i B ) e. V -> ( A = B -> ( A e. _V /\ B e. _V ) ) )
3 bj-opelidb 
 |-  ( <. A , B >. e. _I <-> ( ( A e. _V /\ B e. _V ) /\ A = B ) )
4 simpr 
 |-  ( ( ( A e. _V /\ B e. _V ) /\ A = B ) -> A = B )
5 ancr 
 |-  ( ( A = B -> ( A e. _V /\ B e. _V ) ) -> ( A = B -> ( ( A e. _V /\ B e. _V ) /\ A = B ) ) )
6 4 5 impbid2 
 |-  ( ( A = B -> ( A e. _V /\ B e. _V ) ) -> ( ( ( A e. _V /\ B e. _V ) /\ A = B ) <-> A = B ) )
7 3 6 bitrid 
 |-  ( ( A = B -> ( A e. _V /\ B e. _V ) ) -> ( <. A , B >. e. _I <-> A = B ) )
8 2 7 syl 
 |-  ( ( A i^i B ) e. V -> ( <. A , B >. e. _I <-> A = B ) )