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

Proof

Step Hyp Ref Expression
1 bj-inexeqex ( ( ( 𝐴𝐵 ) ∈ 𝑉𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
2 1 ex ( ( 𝐴𝐵 ) ∈ 𝑉 → ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
3 bj-opelidb ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) )
4 simpr ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
5 ancr ( ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ) )
6 4 5 impbid2 ( ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ↔ 𝐴 = 𝐵 ) )
7 3 6 syl5bb ( ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )
8 2 7 syl ( ( 𝐴𝐵 ) ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )