Theorem bj-opelidb

Description: Characterization of the ordered pair elements of the identity relation.

Remark: in deduction-style proofs, one could save a few syntactic steps by using another antecedent than T. which already appears in the proof. Here for instance this could be the definition _I = { <. x , y >. | x = y } but this would make the proof less easy to read. (Contributed by BJ, 27-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
2	1	a1i	⊢ ( ⊤ → I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } )
3		eqeq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
4	3	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝐵 ) )
5	2 4	opelopabbv	⊢ ( ⊤ → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) ) )
6	5	mptru	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐴 = 𝐵 ) )