Theorem prcom 4689

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

Syntax hints:   = wceq 1541   ∪ cun 3899  {csn 4580  {cpr 4582

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-pr 4583

This theorem is referenced by:  preq2  4691  tpcoma  4707  tpidm23  4714  prid2g  4718  prid2  4720  prprc2  4723  difprsn2  4757  tpprceq3  4760  tppreqb  4761  ssprsseq  4781  preq2b  4803  preqr2  4805  preq12b  4806  prnebg  4812  preq12nebg  4819  opthprneg  4821  elpreqpr  4823  elpr2elpr  4825  fvpr2g  7137  en2other2  9919  hashprb  14320  joincomALT  18322  meetcomALT  18324  symggen  19399  psgnran  19444  lspprid2  20949  lspexchn2  21086  lspindp2l  21089  lspindp2  21090  lsppratlem1  21102  psgnghm  21535  uvcvvcl  21742  mdetralt  22552  mdetunilem7  22562  uhgr2edg  29281  usgredg4  29290  usgredg2vlem1  29298  usgredg2vlem2  29299  nbupgrel  29418  nbgr2vtx1edg  29423  nbuhgr2vtx1edgblem  29424  nbuhgr2vtx1edgb  29425  nbusgreledg  29426  nbgrssvwo2  29435  nbgrsym  29436  usgrnbcnvfv  29438  edgnbusgreu  29440  nbusgrf1o0  29442  nb3grprlem1  29453  nb3grprlem2  29454  nb3grpr  29455  nb3grpr2  29456  nb3gr2nb  29457  isuvtx  29468  cusgredg  29497  usgredgsscusgredg  29533  1hegrvtxdg1r  29582  1egrvtxdg1r  29584  vdegp1ci  29612  usgr2wlkneq  29829  usgr2trlncl  29833  usgr2pthlem  29836  uspgrn2crct  29881  2wlkdlem6  30004  umgr2adedgspth  30021  wwlks2onsym  30033  clwwlkn2  30119  clwwlknonex2  30184  wlk2v2elem2  30231  uhgr3cyclexlem  30256  umgr3cyclex  30258  frcond1  30341  frcond3  30344  frgr3v  30350  3vfriswmgr  30353  1to3vfriswmgr  30355  1to3vfriendship  30356  2pthfrgrrn  30357  3cyclfrgrrn1  30360  4cycl2v2nb  30364  n4cyclfrgr  30366  frgrnbnb  30368  frgrncvvdeqlem3  30376  frgrncvvdeqlem6  30379  frgrwopregbsn  30392  frgrwopreglem5ALT  30397  fusgr2wsp2nb  30409  2clwwlk2clwwlklem  30421  indf  32934  indpreima  32947  indsupp  32949  pmtrprfv2  33170  cyc3genpmlem  33233  measxun2  34367  measssd  34372  revwlk  35319  cusgr3cyclex  35330  2cycl2d  35333  poimirlem9  37830  poimirlem15  37836  dihprrn  41686  dvh3dim  41706  dvh3dim3N  41709  lcfrlem21  41823  mapdindp4  41983  mapdh6eN  42000  mapdh7dN  42010  mapdh8ab  42037  mapdh8ad  42039  mapdh8b  42040  mapdh8e  42044  hdmap1l6e  42074  hdmap11lem2  42102  sprsymrelf  47741  paireqne  47757  reuopreuprim  47772  dfodd5  47906  clnbupgrel  48080  clnbgrsym  48084  grtriproplem  48185  grtrif1o  48188  grtriclwlk3  48191  cycl3grtrilem  48192  usgrgrtrirex  48196  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  grlimprclnbgr  48242  grlimprclnbgrvtx  48245  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  gpgprismgriedgdmss  48298  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgedg2ov  48312  gpgedg2iv  48313  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem8  48348  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5  48369  pgnbgreunbgr  48371  pgn4cyclex  48372  glbprlem  49210  toslat  49227