Theorem prcom 3772

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 3367	. 2 ⊢ ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2		df-pr 3701	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3		df-pr 3701	. 2 ⊢ {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
4	1, 2, 3	3eqtr4i 2265	1 ⊢ {𝐴, 𝐵} = {𝐵, 𝐴}

Syntax hints:   = wceq 1398   ∪ cun 3212  {csn 3694  {cpr 3695

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-pr 3701

This theorem is referenced by:  preq2  3774  tpcoma  3790  tpidm23  3797  prid2g  3801  prid2  3803  prprc2  3806  difprsn2  3839  ssprsseq  3861  preqr2g  3876  preqr2  3878  preq12b  3879  elpr2elpr  3885  fvpr2  5894  fvpr2g  5896  pr2cv2  7506  en2other2  7512  maxcom  11913  mincom  11939  xrmax2sup  11964  xrmaxltsup  11968  xrmaxadd  11971  xrbdtri  11986  lspprid2  14686  qtopbasss  15512  uhgr2edg  16327  usgredg4  16336  usgredg2vlem1  16343  usgredg2vlem2  16344  1hegrvtxdg1rfi  16431  vdegp1cid  16437  clwwlkn2  16542  clwwlknonex2  16560