Theorem prcom 4692

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

Syntax hints:   = wceq 1540   ∪ cun 3909  {csn 4585  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-pr 4588

This theorem is referenced by:  preq2  4694  tpcoma  4710  tpidm23  4717  prid2g  4721  prid2  4723  prprc2  4726  difprsn2  4761  tpprceq3  4764  tppreqb  4765  ssprsseq  4785  preq2b  4807  preqr2  4809  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpreqpr  4827  elpr2elpr  4829  fvpr2g  7147  en2other2  9938  hashprb  14338  joincomALT  18336  meetcomALT  18338  symggen  19376  psgnran  19421  lspprid2  20880  lspexchn2  21017  lspindp2l  21020  lspindp2  21021  lsppratlem1  21033  psgnghm  21465  uvcvvcl  21672  mdetralt  22471  mdetunilem7  22481  uhgr2edg  29111  usgredg4  29120  usgredg2vlem1  29128  usgredg2vlem2  29129  nbupgrel  29248  nbgr2vtx1edg  29253  nbuhgr2vtx1edgblem  29254  nbuhgr2vtx1edgb  29255  nbusgreledg  29256  nbgrssvwo2  29265  nbgrsym  29266  usgrnbcnvfv  29268  edgnbusgreu  29270  nbusgrf1o0  29272  nb3grprlem1  29283  nb3grprlem2  29284  nb3grpr  29285  nb3grpr2  29286  nb3gr2nb  29287  isuvtx  29298  cusgredg  29327  usgredgsscusgredg  29363  1hegrvtxdg1r  29412  1egrvtxdg1r  29414  vdegp1ci  29442  usgr2wlkneq  29659  usgr2trlncl  29663  usgr2pthlem  29666  uspgrn2crct  29711  2wlkdlem6  29834  umgr2adedgspth  29851  wwlks2onsym  29861  clwwlkn2  29946  clwwlknonex2  30011  wlk2v2elem2  30058  uhgr3cyclexlem  30083  umgr3cyclex  30085  frcond1  30168  frcond3  30171  frgr3v  30177  3vfriswmgr  30180  1to3vfriswmgr  30182  1to3vfriendship  30183  2pthfrgrrn  30184  3cyclfrgrrn1  30187  4cycl2v2nb  30191  n4cyclfrgr  30193  frgrnbnb  30195  frgrncvvdeqlem3  30203  frgrncvvdeqlem6  30206  frgrwopregbsn  30219  frgrwopreglem5ALT  30224  fusgr2wsp2nb  30236  2clwwlk2clwwlklem  30248  indf  32751  indpreima  32761  indsupp  32763  pmtrprfv2  33018  cyc3genpmlem  33081  measxun2  34173  measssd  34178  revwlk  35085  cusgr3cyclex  35096  2cycl2d  35099  poimirlem9  37596  poimirlem15  37602  dihprrn  41393  dvh3dim  41413  dvh3dim3N  41416  lcfrlem21  41530  mapdindp4  41690  mapdh6eN  41707  mapdh7dN  41717  mapdh8ab  41744  mapdh8ad  41746  mapdh8b  41747  mapdh8e  41751  hdmap1l6e  41781  hdmap11lem2  41809  sprsymrelf  47469  paireqne  47485  reuopreuprim  47500  dfodd5  47634  clnbupgrel  47808  clnbgrsym  47811  grtriproplem  47911  grtrif1o  47914  grtriclwlk3  47917  cycl3grtrilem  47918  usgrgrtrirex  47922  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  gpgprismgriedgdmss  48016  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgedg2ov  48030  gpgedg2iv  48031  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx03star  48044  gpg5nbgr3star  48045  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem8  48065  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5  48086  pgnbgreunbgr  48088  pgn4cyclex  48089  glbprlem  48926  toslat  48943