Theorem opcom

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

	Ref	Expression
Hypotheses	opcom.1	|- A e. _V
	opcom.2	|- B e. _V
Assertion	opcom	|- ( <. A , B >. = <. B , A >. <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		opcom.1	|- A e. _V
2		opcom.2	|- B e. _V
3	1 2	opth	|- ( <. A , B >. = <. B , A >. <-> ( A = B /\ B = A ) )
4		eqcom	|- ( B = A <-> A = B )
5	4	anbi2i	|- ( ( A = B /\ B = A ) <-> ( A = B /\ A = B ) )
6		anidm	|- ( ( A = B /\ A = B ) <-> A = B )
7	3 5 6	3bitri	|- ( <. A , B >. = <. B , A >. <-> A = B )