Theorem bj-opelidb1

Description: Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Assertion	bj-opelidb1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		an32	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) ∧ 𝐵 ∈ V ) )
2		bj-opelidb	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) )
3		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
4	3	biimpac	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
5	4	pm4.71i	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) ∧ 𝐵 ∈ V ) )
6	1 2 5	3bitr4i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) )