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	bitrid	⊢ ( ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )
8	2 7	syl	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )