Theorem prcom 4730

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

Syntax hints:   = wceq 1541   ∪ cun 3943  {csn 4623  {cpr 4625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3950  df-pr 4626

This theorem is referenced by:  preq2  4732  tpcoma  4748  tpidm23  4755  prid2g  4759  prid2  4761  prprc2  4764  difprsn2  4798  tpprceq3  4801  tppreqb  4802  ssprsseq  4822  preq2b  4842  preqr2  4844  preq12b  4845  prnebg  4850  preq12nebg  4857  opthprneg  4859  elpreqpr  4861  elpr2elpr  4863  fvpr2g  7174  fvpr2gOLD  7175  fvpr2OLD  7179  en2other2  9988  hashprb  14341  joincomALT  18338  meetcomALT  18340  symggen  19304  psgnran  19349  lspprid2  20560  lspexchn2  20695  lspindp2l  20698  lspindp2  20699  lsppratlem1  20711  psgnghm  21068  uvcvvcl  21277  mdetralt  22041  mdetunilem7  22051  uhgr2edg  28394  usgredg4  28403  usgredg2vlem1  28411  usgredg2vlem2  28412  nbupgrel  28531  nbgr2vtx1edg  28536  nbuhgr2vtx1edgblem  28537  nbuhgr2vtx1edgb  28538  nbusgreledg  28539  nbgrssvwo2  28548  nbgrsym  28549  usgrnbcnvfv  28551  edgnbusgreu  28553  nbusgrf1o0  28555  nb3grprlem1  28566  nb3grprlem2  28567  nb3grpr  28568  nb3grpr2  28569  nb3gr2nb  28570  isuvtx  28581  cusgredg  28610  usgredgsscusgredg  28645  1hegrvtxdg1r  28694  1egrvtxdg1r  28696  vdegp1ci  28724  usgr2wlkneq  28942  usgr2trlncl  28946  usgr2pthlem  28949  uspgrn2crct  28991  2wlkdlem6  29114  umgr2adedgspth  29131  wwlks2onsym  29141  clwwlkn2  29226  clwwlknonex2  29291  wlk2v2elem2  29338  uhgr3cyclexlem  29363  umgr3cyclex  29365  frcond1  29448  frcond3  29451  frgr3v  29457  3vfriswmgr  29460  1to3vfriswmgr  29462  1to3vfriendship  29463  2pthfrgrrn  29464  3cyclfrgrrn1  29467  4cycl2v2nb  29471  n4cyclfrgr  29473  frgrnbnb  29475  frgrncvvdeqlem3  29483  frgrncvvdeqlem6  29486  frgrwopregbsn  29499  frgrwopreglem5ALT  29504  fusgr2wsp2nb  29516  2clwwlk2clwwlklem  29528  pmtrprfv2  32184  cyc3genpmlem  32245  indf  32908  indpreima  32918  measxun2  33103  measssd  33108  revwlk  34010  cusgr3cyclex  34022  2cycl2d  34025  poimirlem9  36365  poimirlem15  36371  dihprrn  40166  dvh3dim  40186  dvh3dim3N  40189  lcfrlem21  40303  mapdindp4  40463  mapdh6eN  40480  mapdh7dN  40490  mapdh8ab  40517  mapdh8ad  40519  mapdh8b  40520  mapdh8e  40524  hdmap1l6e  40554  hdmap11lem2  40582  sprsymrelf  45999  paireqne  46015  reuopreuprim  46030  dfodd5  46164  glbprlem  47310  toslat  47319