Metamath Proof Explorer


Theorem opcom

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

Ref Expression
Hypotheses opcom.1 AV
opcom.2 BV
Assertion opcom AB=BAA=B

Proof

Step Hyp Ref Expression
1 opcom.1 AV
2 opcom.2 BV
3 1 2 opth AB=BAA=BB=A
4 eqcom B=AA=B
5 4 anbi2i A=BB=AA=BA=B
6 anidm A=BA=BA=B
7 3 5 6 3bitri AB=BAA=B