Theorem opcom

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

	Ref	Expression
Hypotheses	opcom.1	$$⊢A\in \mathrm{V}$$
	opcom.2	$$⊢B\in \mathrm{V}$$
Assertion	opcom	$$⊢⟨A,B⟩=⟨B,A⟩\leftrightarrow A=B$$

Proof

Step	Hyp	Ref	Expression
1		opcom.1	$$⊢A\in \mathrm{V}$$
2		opcom.2	$$⊢B\in \mathrm{V}$$
3	1 2	opth	$$⊢⟨A,B⟩=⟨B,A⟩\leftrightarrow \left(A=B\wedge B=A\right)$$
4		eqcom	$$⊢B=A\leftrightarrow A=B$$
5	4	anbi2i	$$⊢\left(A=B\wedge B=A\right)\leftrightarrow \left(A=B\wedge A=B\right)$$
6		anidm	$$⊢\left(A=B\wedge A=B\right)\leftrightarrow A=B$$
7	3 5 6	3bitri	$$⊢⟨A,B⟩=⟨B,A⟩\leftrightarrow A=B$$