Theorem prcom 4737

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

Syntax hints:   = wceq 1537   ∪ cun 3961  {csn 4631  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-pr 4634

This theorem is referenced by:  preq2  4739  tpcoma  4755  tpidm23  4762  prid2g  4766  prid2  4768  prprc2  4771  difprsn2  4806  tpprceq3  4809  tppreqb  4810  ssprsseq  4830  preq2b  4852  preqr2  4854  preq12b  4855  prnebg  4861  preq12nebg  4868  opthprneg  4870  elpreqpr  4872  elpr2elpr  4874  fvpr2g  7211  en2other2  10047  hashprb  14433  joincomALT  18459  meetcomALT  18461  symggen  19503  psgnran  19548  lspprid2  21014  lspexchn2  21151  lspindp2l  21154  lspindp2  21155  lsppratlem1  21167  psgnghm  21616  uvcvvcl  21825  mdetralt  22630  mdetunilem7  22640  uhgr2edg  29240  usgredg4  29249  usgredg2vlem1  29257  usgredg2vlem2  29258  nbupgrel  29377  nbgr2vtx1edg  29382  nbuhgr2vtx1edgblem  29383  nbuhgr2vtx1edgb  29384  nbusgreledg  29385  nbgrssvwo2  29394  nbgrsym  29395  usgrnbcnvfv  29397  edgnbusgreu  29399  nbusgrf1o0  29401  nb3grprlem1  29412  nb3grprlem2  29413  nb3grpr  29414  nb3grpr2  29415  nb3gr2nb  29416  isuvtx  29427  cusgredg  29456  usgredgsscusgredg  29492  1hegrvtxdg1r  29541  1egrvtxdg1r  29543  vdegp1ci  29571  usgr2wlkneq  29789  usgr2trlncl  29793  usgr2pthlem  29796  uspgrn2crct  29838  2wlkdlem6  29961  umgr2adedgspth  29978  wwlks2onsym  29988  clwwlkn2  30073  clwwlknonex2  30138  wlk2v2elem2  30185  uhgr3cyclexlem  30210  umgr3cyclex  30212  frcond1  30295  frcond3  30298  frgr3v  30304  3vfriswmgr  30307  1to3vfriswmgr  30309  1to3vfriendship  30310  2pthfrgrrn  30311  3cyclfrgrrn1  30314  4cycl2v2nb  30318  n4cyclfrgr  30320  frgrnbnb  30322  frgrncvvdeqlem3  30330  frgrncvvdeqlem6  30333  frgrwopregbsn  30346  frgrwopreglem5ALT  30351  fusgr2wsp2nb  30363  2clwwlk2clwwlklem  30375  pmtrprfv2  33091  cyc3genpmlem  33154  indf  33996  indpreima  34006  measxun2  34191  measssd  34196  revwlk  35109  cusgr3cyclex  35121  2cycl2d  35124  poimirlem9  37616  poimirlem15  37622  dihprrn  41409  dvh3dim  41429  dvh3dim3N  41432  lcfrlem21  41546  mapdindp4  41706  mapdh6eN  41723  mapdh7dN  41733  mapdh8ab  41760  mapdh8ad  41762  mapdh8b  41763  mapdh8e  41767  hdmap1l6e  41797  hdmap11lem2  41825  sprsymrelf  47420  paireqne  47436  reuopreuprim  47451  dfodd5  47585  clnbupgrel  47759  clnbgrsym  47762  grtriproplem  47844  grtrif1o  47847  grtriclwlk3  47850  usgrgrtrirex  47853  isubgr3stgrlem6  47874  isubgr3stgrlem7  47875  usgrexmpl2nb1  47927  usgrexmpl2nb2  47928  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  gpgedgvtx0  47954  gpgedgvtx1  47955  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx03star  47971  gpg5nbgr3star  47972  glbprlem  48762  toslat  48771