This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prcom

Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion prcom ⊢ A B = B A

Proof

Step Hyp Ref Expression
1 uncom ⊢ A ∪ B = B ∪ A
2 df-pr ⊢ A B = A ∪ B
3 df-pr ⊢ B A = B ∪ A
4 1 2 3 3eqtr4i ⊢ A B = B A