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 ∈ V → A B ∈ I ↾ V ↔ A = B

Proof

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