Theorem prcom 4677

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

Syntax hints:   = wceq 1542   ∪ cun 3888  {csn 4568  {cpr 4570

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-pr 4571

This theorem is referenced by:  preq2  4679  tpcoma  4695  tpidm23  4702  prid2g  4706  prid2  4708  prprc2  4711  difprsn2  4745  tpprceq3  4748  tppreqb  4749  ssprsseq  4769  preq2b  4791  preqr2  4793  preq12b  4794  prnebg  4800  preq12nebg  4807  opthprneg  4809  elpreqpr  4811  elpr2elpr  4813  fvpr2g  7139  en2other2  9922  indf  12156  hashprb  14350  joincomALT  18356  meetcomALT  18358  symggen  19436  psgnran  19481  lspprid2  20984  lspexchn2  21121  lspindp2l  21124  lspindp2  21125  lsppratlem1  21137  psgnghm  21570  uvcvvcl  21777  mdetralt  22583  mdetunilem7  22593  uhgr2edg  29291  usgredg4  29300  usgredg2vlem1  29308  usgredg2vlem2  29309  nbupgrel  29428  nbgr2vtx1edg  29433  nbuhgr2vtx1edgblem  29434  nbuhgr2vtx1edgb  29435  nbusgreledg  29436  nbgrssvwo2  29445  nbgrsym  29446  usgrnbcnvfv  29448  edgnbusgreu  29450  nbusgrf1o0  29452  nb3grprlem1  29463  nb3grprlem2  29464  nb3grpr  29465  nb3grpr2  29466  nb3gr2nb  29467  isuvtx  29478  cusgredg  29507  usgredgsscusgredg  29543  1hegrvtxdg1r  29592  1egrvtxdg1r  29594  vdegp1ci  29622  usgr2wlkneq  29839  usgr2trlncl  29843  usgr2pthlem  29846  uspgrn2crct  29891  2wlkdlem6  30014  umgr2adedgspth  30031  wwlks2onsym  30043  clwwlkn2  30129  clwwlknonex2  30194  wlk2v2elem2  30241  uhgr3cyclexlem  30266  umgr3cyclex  30268  frcond1  30351  frcond3  30354  frgr3v  30360  3vfriswmgr  30363  1to3vfriswmgr  30365  1to3vfriendship  30366  2pthfrgrrn  30367  3cyclfrgrrn1  30370  4cycl2v2nb  30374  n4cyclfrgr  30376  frgrnbnb  30378  frgrncvvdeqlem3  30386  frgrncvvdeqlem6  30389  frgrwopregbsn  30402  frgrwopreglem5ALT  30407  fusgr2wsp2nb  30419  2clwwlk2clwwlklem  30431  indpreima  32940  indsupp  32942  pmtrprfv2  33164  cyc3genpmlem  33227  measxun2  34370  measssd  34375  revwlk  35323  cusgr3cyclex  35334  2cycl2d  35337  poimirlem9  37964  poimirlem15  37970  dihprrn  41886  dvh3dim  41906  dvh3dim3N  41909  lcfrlem21  42023  mapdindp4  42183  mapdh6eN  42200  mapdh7dN  42210  mapdh8ab  42237  mapdh8ad  42239  mapdh8b  42240  mapdh8e  42244  hdmap1l6e  42274  hdmap11lem2  42302  sprsymrelf  47967  paireqne  47983  reuopreuprim  47998  dfodd5  48148  clnbupgrel  48322  clnbgrsym  48326  grtriproplem  48427  grtrif1o  48430  grtriclwlk3  48433  cycl3grtrilem  48434  usgrgrtrirex  48438  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  grlimprclnbgr  48484  grlimprclnbgrvtx  48487  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgprismgriedgdmss  48540  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgedg2ov  48554  gpgedg2iv  48555  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem8  48590  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  pgnbgreunbgr  48613  pgn4cyclex  48614  glbprlem  49452  toslat  49469