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	bitrid	|- ( A e. V -> ( <. A , B >. e. ( _I i^i ( V X. V ) ) <-> A = B ) )
18	2 17	bitrid	|- ( A e. V -> ( <. A , B >. e. ( _I |` V ) <-> A = B ) )