Theorem prcom 4684

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

Syntax hints:   = wceq 1541   ∪ cun 3895  {csn 4575  {cpr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-pr 4578

This theorem is referenced by:  preq2  4686  tpcoma  4702  tpidm23  4709  prid2g  4713  prid2  4715  prprc2  4718  difprsn2  4752  tpprceq3  4755  tppreqb  4756  ssprsseq  4776  preq2b  4798  preqr2  4800  preq12b  4801  prnebg  4807  preq12nebg  4814  opthprneg  4816  elpreqpr  4818  elpr2elpr  4820  fvpr2g  7131  en2other2  9906  hashprb  14310  joincomALT  18311  meetcomALT  18313  symggen  19388  psgnran  19433  lspprid2  20937  lspexchn2  21074  lspindp2l  21077  lspindp2  21078  lsppratlem1  21090  psgnghm  21523  uvcvvcl  21730  mdetralt  22529  mdetunilem7  22539  uhgr2edg  29193  usgredg4  29202  usgredg2vlem1  29210  usgredg2vlem2  29211  nbupgrel  29330  nbgr2vtx1edg  29335  nbuhgr2vtx1edgblem  29336  nbuhgr2vtx1edgb  29337  nbusgreledg  29338  nbgrssvwo2  29347  nbgrsym  29348  usgrnbcnvfv  29350  edgnbusgreu  29352  nbusgrf1o0  29354  nb3grprlem1  29365  nb3grprlem2  29366  nb3grpr  29367  nb3grpr2  29368  nb3gr2nb  29369  isuvtx  29380  cusgredg  29409  usgredgsscusgredg  29445  1hegrvtxdg1r  29494  1egrvtxdg1r  29496  vdegp1ci  29524  usgr2wlkneq  29741  usgr2trlncl  29745  usgr2pthlem  29748  uspgrn2crct  29793  2wlkdlem6  29916  umgr2adedgspth  29933  wwlks2onsym  29945  clwwlkn2  30031  clwwlknonex2  30096  wlk2v2elem2  30143  uhgr3cyclexlem  30168  umgr3cyclex  30170  frcond1  30253  frcond3  30256  frgr3v  30262  3vfriswmgr  30265  1to3vfriswmgr  30267  1to3vfriendship  30268  2pthfrgrrn  30269  3cyclfrgrrn1  30272  4cycl2v2nb  30276  n4cyclfrgr  30278  frgrnbnb  30280  frgrncvvdeqlem3  30288  frgrncvvdeqlem6  30291  frgrwopregbsn  30304  frgrwopreglem5ALT  30309  fusgr2wsp2nb  30321  2clwwlk2clwwlklem  30333  indf  32843  indpreima  32853  indsupp  32855  pmtrprfv2  33064  cyc3genpmlem  33127  measxun2  34230  measssd  34235  revwlk  35176  cusgr3cyclex  35187  2cycl2d  35190  poimirlem9  37675  poimirlem15  37681  dihprrn  41531  dvh3dim  41551  dvh3dim3N  41554  lcfrlem21  41668  mapdindp4  41828  mapdh6eN  41845  mapdh7dN  41855  mapdh8ab  41882  mapdh8ad  41884  mapdh8b  41885  mapdh8e  41889  hdmap1l6e  41919  hdmap11lem2  41947  sprsymrelf  47600  paireqne  47616  reuopreuprim  47631  dfodd5  47765  clnbupgrel  47939  clnbgrsym  47943  grtriproplem  48044  grtrif1o  48047  grtriclwlk3  48050  cycl3grtrilem  48051  usgrgrtrirex  48055  isubgr3stgrlem6  48076  isubgr3stgrlem7  48077  grlimprclnbgr  48101  grlimprclnbgrvtx  48104  usgrexmpl2nb1  48137  usgrexmpl2nb2  48138  usgrexmpl2nb3  48139  usgrexmpl2nb4  48140  usgrexmpl2nb5  48141  gpgprismgriedgdmss  48157  gpgedgvtx0  48166  gpgedgvtx1  48167  gpgedg2ov  48171  gpgedg2iv  48172  gpg5nbgrvtx03starlem3  48175  gpg5nbgrvtx03star  48185  gpg5nbgr3star  48186  gpgprismgr4cycllem3  48202  gpgprismgr4cycllem8  48207  pgnbgreunbgrlem1  48218  pgnbgreunbgrlem2lem3  48221  pgnbgreunbgrlem2  48222  pgnbgreunbgrlem4  48224  pgnbgreunbgrlem5  48228  pgnbgreunbgr  48230  pgn4cyclex  48231  glbprlem  49070  toslat  49087