Theorem prcom 3694

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

Assertion

Ref	Expression
prcom	⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom

Step	Hyp	Ref	Expression
1		uncom 3303	. 2 ⊢ ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2		df-pr 3625	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3		df-pr 3625	. 2 ⊢ {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
4	1, 2, 3	3eqtr4i 2224	1 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Syntax hints:   = wceq 1364   ∪ cun 3151  {csn 3618  {cpr 3619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-pr 3625

This theorem is referenced by:  preq2  3696  tpcoma  3712  tpidm23  3719  prid2g  3723  prid2  3725  prprc2  3727  difprsn2  3758  preqr2g  3793  preqr2  3795  preq12b  3796  fvpr2  5763  fvpr2g  5765  en2other2  7256  maxcom  11347  mincom  11372  xrmax2sup  11397  xrmaxltsup  11401  xrmaxadd  11404  xrbdtri  11419  lspprid2  13908  qtopbasss  14689