Theorem opcom

Description: An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009)

	Ref	Expression
Hypotheses	opcom.1	⊢ 𝐴 ∈ V
	opcom.2	⊢ 𝐵 ∈ V
Assertion	opcom	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ ↔ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		opcom.1	⊢ 𝐴 ∈ V
2		opcom.2	⊢ 𝐵 ∈ V
3	1 2	opth	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐴 ) )
4		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
5	4	anbi2i	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐴 = 𝐵 ) )
6		anidm	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 = 𝐵 ) ↔ 𝐴 = 𝐵 )
7	3 5 6	3bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ ↔ 𝐴 = 𝐵 )