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 } u. { B } ) = ( { B } u. { A } )
2 df-pr 
 |-  { A , B } = ( { A } u. { B } )
3 df-pr 
 |-  { B , A } = ( { B } u. { A } )
4 1 2 3 3eqtr4i 
 |-  { A , B } = { B , A }