Theorem prcom 4744

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

Assertion

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

Proof of Theorem prcom

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

Syntax hints:   = wceq 1534   ∪ cun 3957  {csn 4636  {cpr 4638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-un 3964  df-pr 4639

This theorem is referenced by:  preq2  4746  tpcoma  4762  tpidm23  4769  prid2g  4773  prid2  4775  prprc2  4778  difprsn2  4813  tpprceq3  4816  tppreqb  4817  ssprsseq  4837  preq2b  4859  preqr2  4861  preq12b  4862  prnebg  4867  preq12nebg  4874  opthprneg  4876  elpreqpr  4878  elpr2elpr  4880  fvpr2g  7210  fvpr2gOLD  7211  fvpr2OLD  7215  en2other2  10059  hashprb  14426  joincomALT  18447  meetcomALT  18449  symggen  19490  psgnran  19535  lspprid2  20997  lspexchn2  21134  lspindp2l  21137  lspindp2  21138  lsppratlem1  21150  psgnghm  21598  uvcvvcl  21807  mdetralt  22624  mdetunilem7  22634  uhgr2edg  29167  usgredg4  29176  usgredg2vlem1  29184  usgredg2vlem2  29185  nbupgrel  29304  nbgr2vtx1edg  29309  nbuhgr2vtx1edgblem  29310  nbuhgr2vtx1edgb  29311  nbusgreledg  29312  nbgrssvwo2  29321  nbgrsym  29322  usgrnbcnvfv  29324  edgnbusgreu  29326  nbusgrf1o0  29328  nb3grprlem1  29339  nb3grprlem2  29340  nb3grpr  29341  nb3grpr2  29342  nb3gr2nb  29343  isuvtx  29354  cusgredg  29383  usgredgsscusgredg  29419  1hegrvtxdg1r  29468  1egrvtxdg1r  29470  vdegp1ci  29498  usgr2wlkneq  29716  usgr2trlncl  29720  usgr2pthlem  29723  uspgrn2crct  29765  2wlkdlem6  29888  umgr2adedgspth  29905  wwlks2onsym  29915  clwwlkn2  30000  clwwlknonex2  30065  wlk2v2elem2  30112  uhgr3cyclexlem  30137  umgr3cyclex  30139  frcond1  30222  frcond3  30225  frgr3v  30231  3vfriswmgr  30234  1to3vfriswmgr  30236  1to3vfriendship  30237  2pthfrgrrn  30238  3cyclfrgrrn1  30241  4cycl2v2nb  30245  n4cyclfrgr  30247  frgrnbnb  30249  frgrncvvdeqlem3  30257  frgrncvvdeqlem6  30260  frgrwopregbsn  30273  frgrwopreglem5ALT  30278  fusgr2wsp2nb  30290  2clwwlk2clwwlklem  30302  pmtrprfv2  32995  cyc3genpmlem  33058  indf  33886  indpreima  33896  measxun2  34081  measssd  34086  revwlk  34990  cusgr3cyclex  35002  2cycl2d  35005  poimirlem9  37368  poimirlem15  37374  dihprrn  41163  dvh3dim  41183  dvh3dim3N  41186  lcfrlem21  41300  mapdindp4  41460  mapdh6eN  41477  mapdh7dN  41487  mapdh8ab  41514  mapdh8ad  41516  mapdh8b  41517  mapdh8e  41521  hdmap1l6e  41551  hdmap11lem2  41579  sprsymrelf  47128  paireqne  47144  reuopreuprim  47159  dfodd5  47293  clnbupgrel  47466  clnbgrsym  47469  grtriproplem  47573  grtrif1o  47576  grtriclwlk3  47579  glbprlem  48371  toslat  48380