Theorem prcom 4667

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

Syntax hints:   = wceq 1533   ∪ cun 3933  {csn 4566  {cpr 4568

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-pr 4569

This theorem is referenced by:  preq2  4669  tpcoma  4685  tpidm23  4692  prid2g  4696  prid2  4698  prprc2  4701  difprsn2  4733  tpprceq3  4736  tppreqb  4737  ssprsseq  4757  preq2b  4777  preqr2  4779  preq12b  4780  prnebg  4785  preq12nebg  4792  opthprneg  4794  elpreqpr  4796  elpr2elpr  4798  fvpr2  6952  fvpr2g  6954  en2other2  9434  hashprb  13757  joincomALT  17638  meetcomALT  17640  symggen  18597  psgnran  18642  lspprid2  19769  lspexchn2  19902  lspindp2l  19905  lspindp2  19906  lsppratlem1  19918  psgnghm  20723  uvcvvcl  20930  mdetralt  21216  mdetunilem7  21226  uhgr2edg  26989  usgredg4  26998  usgredg2vlem1  27006  usgredg2vlem2  27007  nbupgrel  27126  nbgr2vtx1edg  27131  nbuhgr2vtx1edgblem  27132  nbuhgr2vtx1edgb  27133  nbusgreledg  27134  nbgrssvwo2  27143  nbgrsym  27144  usgrnbcnvfv  27146  edgnbusgreu  27148  nbusgrf1o0  27150  nb3grprlem1  27161  nb3grprlem2  27162  nb3grpr  27163  nb3grpr2  27164  nb3gr2nb  27165  isuvtx  27176  cusgredg  27205  usgredgsscusgredg  27240  1hegrvtxdg1r  27289  1egrvtxdg1r  27291  vdegp1ci  27319  usgr2wlkneq  27536  usgr2trlncl  27540  usgr2pthlem  27543  uspgrn2crct  27585  2wlkdlem6  27709  umgr2adedgspth  27726  wwlks2onsym  27736  clwwlkn2  27821  clwwlknonex2  27887  wlk2v2elem2  27934  uhgr3cyclexlem  27959  umgr3cyclex  27961  frcond1  28044  frcond3  28047  frgr3v  28053  3vfriswmgr  28056  1to3vfriswmgr  28058  1to3vfriendship  28059  2pthfrgrrn  28060  3cyclfrgrrn1  28063  4cycl2v2nb  28067  n4cyclfrgr  28069  frgrnbnb  28071  frgrncvvdeqlem3  28079  frgrncvvdeqlem6  28082  frgrwopregbsn  28095  frgrwopreglem5ALT  28100  fusgr2wsp2nb  28112  2clwwlk2clwwlklem  28124  pmtrprfv2  30732  cyc3genpmlem  30793  indf  31274  indpreima  31284  measxun2  31469  measssd  31474  revwlk  32371  cusgr3cyclex  32383  2cycl2d  32386  poimirlem9  34900  poimirlem15  34906  dihprrn  38561  dvh3dim  38581  dvh3dim3N  38584  lcfrlem21  38698  mapdindp4  38858  mapdh6eN  38875  mapdh7dN  38885  mapdh8ab  38912  mapdh8ad  38914  mapdh8b  38915  mapdh8e  38919  hdmap1l6e  38949  hdmap11lem2  38977  sprsymrelf  43656  paireqne  43672  reuopreuprim  43687  dfodd5  43824