Metamath Proof Explorer


Theorem bj-opelidres

Description: Characterization of the ordered pairs in the restricted identity relation when the intersection of their component belongs to the restricting class. TODO: prove bj-idreseq from it. (Contributed by BJ, 29-Mar-2020)

Ref Expression
Assertion bj-opelidres
|- ( A e. V -> ( <. A , B >. e. ( _I |` V ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 bj-idres
 |-  ( _I |` V ) = ( _I i^i ( V X. V ) )
2 1 eleq2i
 |-  ( <. A , B >. e. ( _I |` V ) <-> <. A , B >. e. ( _I i^i ( V X. V ) ) )
3 elin
 |-  ( <. A , B >. e. ( _I i^i ( V X. V ) ) <-> ( <. A , B >. e. _I /\ <. A , B >. e. ( V X. V ) ) )
4 inex1g
 |-  ( A e. V -> ( A i^i B ) e. _V )
5 bj-opelid
 |-  ( ( A i^i B ) e. _V -> ( <. A , B >. e. _I <-> A = B ) )
6 4 5 syl
 |-  ( A e. V -> ( <. A , B >. e. _I <-> A = B ) )
7 opelxp
 |-  ( <. A , B >. e. ( V X. V ) <-> ( A e. V /\ B e. V ) )
8 7 a1i
 |-  ( A e. V -> ( <. A , B >. e. ( V X. V ) <-> ( A e. V /\ B e. V ) ) )
9 6 8 anbi12d
 |-  ( A e. V -> ( ( <. A , B >. e. _I /\ <. A , B >. e. ( V X. V ) ) <-> ( A = B /\ ( A e. V /\ B e. V ) ) ) )
10 simpl
 |-  ( ( A = B /\ ( A e. V /\ B e. V ) ) -> A = B )
11 eleq1
 |-  ( A = B -> ( A e. V <-> B e. V ) )
12 11 biimpcd
 |-  ( A e. V -> ( A = B -> B e. V ) )
13 12 anc2li
 |-  ( A e. V -> ( A = B -> ( A e. V /\ B e. V ) ) )
14 13 ancld
 |-  ( A e. V -> ( A = B -> ( A = B /\ ( A e. V /\ B e. V ) ) ) )
15 10 14 impbid2
 |-  ( A e. V -> ( ( A = B /\ ( A e. V /\ B e. V ) ) <-> A = B ) )
16 9 15 bitrd
 |-  ( A e. V -> ( ( <. A , B >. e. _I /\ <. A , B >. e. ( V X. V ) ) <-> A = B ) )
17 3 16 syl5bb
 |-  ( A e. V -> ( <. A , B >. e. ( _I i^i ( V X. V ) ) <-> A = B ) )
18 2 17 syl5bb
 |-  ( A e. V -> ( <. A , B >. e. ( _I |` V ) <-> A = B ) )