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	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ↾ 𝑉 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-idres	⊢ ( I ↾ 𝑉 ) = ( I ∩ ( 𝑉 × 𝑉 ) )
2	1	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ↾ 𝑉 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ∩ ( 𝑉 × 𝑉 ) ) )
3		elin	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ∩ ( 𝑉 × 𝑉 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
4		inex1g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )
5		bj-opelid	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )
6	4 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )
7		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
8	7	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
9	6 8	anbi12d	⊢ ( 𝐴 ∈ 𝑉 → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ) ↔ ( 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
10		simpl	⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 = 𝐵 )
11		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
12	11	biimpcd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐵 ∈ 𝑉 ) )
13	12	anc2li	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
14	13	ancld	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) )
15	10 14	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ↔ 𝐴 = 𝐵 ) )
16	9 15	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑉 × 𝑉 ) ) ↔ 𝐴 = 𝐵 ) )
17	3 16	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ∩ ( 𝑉 × 𝑉 ) ) ↔ 𝐴 = 𝐵 ) )
18	2 17	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( I ↾ 𝑉 ) ↔ 𝐴 = 𝐵 ) )