Theorem prcom 4686

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

Syntax hints:   = wceq 1540   ∪ cun 3903  {csn 4579  {cpr 4581

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 3440  df-un 3910  df-pr 4582

This theorem is referenced by:  preq2  4688  tpcoma  4704  tpidm23  4711  prid2g  4715  prid2  4717  prprc2  4720  difprsn2  4755  tpprceq3  4758  tppreqb  4759  ssprsseq  4779  preq2b  4801  preqr2  4803  preq12b  4804  prnebg  4810  preq12nebg  4817  opthprneg  4819  elpreqpr  4821  elpr2elpr  4823  fvpr2g  7131  en2other2  9922  hashprb  14322  joincomALT  18323  meetcomALT  18325  symggen  19367  psgnran  19412  lspprid2  20919  lspexchn2  21056  lspindp2l  21059  lspindp2  21060  lsppratlem1  21072  psgnghm  21505  uvcvvcl  21712  mdetralt  22511  mdetunilem7  22521  uhgr2edg  29171  usgredg4  29180  usgredg2vlem1  29188  usgredg2vlem2  29189  nbupgrel  29308  nbgr2vtx1edg  29313  nbuhgr2vtx1edgblem  29314  nbuhgr2vtx1edgb  29315  nbusgreledg  29316  nbgrssvwo2  29325  nbgrsym  29326  usgrnbcnvfv  29328  edgnbusgreu  29330  nbusgrf1o0  29332  nb3grprlem1  29343  nb3grprlem2  29344  nb3grpr  29345  nb3grpr2  29346  nb3gr2nb  29347  isuvtx  29358  cusgredg  29387  usgredgsscusgredg  29423  1hegrvtxdg1r  29472  1egrvtxdg1r  29474  vdegp1ci  29502  usgr2wlkneq  29719  usgr2trlncl  29723  usgr2pthlem  29726  uspgrn2crct  29771  2wlkdlem6  29894  umgr2adedgspth  29911  wwlks2onsym  29921  clwwlkn2  30006  clwwlknonex2  30071  wlk2v2elem2  30118  uhgr3cyclexlem  30143  umgr3cyclex  30145  frcond1  30228  frcond3  30231  frgr3v  30237  3vfriswmgr  30240  1to3vfriswmgr  30242  1to3vfriendship  30243  2pthfrgrrn  30244  3cyclfrgrrn1  30247  4cycl2v2nb  30251  n4cyclfrgr  30253  frgrnbnb  30255  frgrncvvdeqlem3  30263  frgrncvvdeqlem6  30266  frgrwopregbsn  30279  frgrwopreglem5ALT  30284  fusgr2wsp2nb  30296  2clwwlk2clwwlklem  30308  indf  32811  indpreima  32821  indsupp  32823  pmtrprfv2  33043  cyc3genpmlem  33106  measxun2  34179  measssd  34184  revwlk  35100  cusgr3cyclex  35111  2cycl2d  35114  poimirlem9  37611  poimirlem15  37617  dihprrn  41408  dvh3dim  41428  dvh3dim3N  41431  lcfrlem21  41545  mapdindp4  41705  mapdh6eN  41722  mapdh7dN  41732  mapdh8ab  41759  mapdh8ad  41761  mapdh8b  41762  mapdh8e  41766  hdmap1l6e  41796  hdmap11lem2  41824  sprsymrelf  47483  paireqne  47499  reuopreuprim  47514  dfodd5  47648  clnbupgrel  47822  clnbgrsym  47826  grtriproplem  47927  grtrif1o  47930  grtriclwlk3  47933  cycl3grtrilem  47934  usgrgrtrirex  47938  isubgr3stgrlem6  47959  isubgr3stgrlem7  47960  grlimprclnbgr  47984  grlimprclnbgrvtx  47987  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  gpgprismgriedgdmss  48040  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgedg2ov  48054  gpgedg2iv  48055  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  gpgprismgr4cycllem3  48085  gpgprismgr4cycllem8  48090  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  pgnbgreunbgr  48113  pgn4cyclex  48114  glbprlem  48953  toslat  48970