Theorem prcom 4688

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

Syntax hints:   = wceq 1559   ∪ cun 3900  {csn 4579  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-pr 4582

This theorem is referenced by:  preq2  4690  tpcoma  4706  tpidm23  4713  prid2g  4717  prid2  4719  prprc2  4722  difprsn2  4758  tpprceq3  4761  tppreqb  4762  ssprsseq  4780  preq2b  4802  preqr2  4804  preq12b  4805  prnebg  4811  preq12nebg  4818  opthprneg  4820  elpreqpr  4822  elpr2elpr  4824  fvpr2g  7169  en2other2  9958  indf  12194  hashprb  14403  joincomALT  18421  meetcomALT  18423  symggen  19500  psgnran  19545  lspprid2  21052  lspexchn2  21188  lspindp2l  21191  lspindp2  21192  lsppratlem1  21204  psgnghm  21619  uvcvvcl  21826  mdetralt  22655  mdetunilem7  22665  uhgr2edg  29365  usgredg4  29374  usgredg2vlem1  29382  usgredg2vlem2  29383  nbupgrel  29502  nbgr2vtx1edg  29507  nbuhgr2vtx1edgblem  29508  nbuhgr2vtx1edgb  29509  nbusgreledg  29510  nbgrssvwo2  29519  nbgrsym  29520  usgrnbcnvfv  29522  edgnbusgreu  29524  nbusgrf1o0  29526  nb3grprlem1  29537  nb3grprlem2  29538  nb3grpr  29539  nb3grpr2  29540  nb3gr2nb  29541  isuvtx  29552  cusgredg  29581  usgredgsscusgredg  29616  1hegrvtxdg1r  29665  1egrvtxdg1r  29667  vdegp1ci  29695  usgr2wlkneq  29912  usgr2trlncl  29916  usgr2pthlem  29919  uspgrn2crct  29964  2wlkdlem6  30087  umgr2adedgspth  30104  wwlks2onsym  30116  clwwlkn2  30202  clwwlknonex2  30267  wlk2v2elem2  30314  uhgr3cyclexlem  30339  umgr3cyclex  30341  frcond1  30424  frcond3  30427  frgr3v  30433  3vfriswmgr  30436  1to3vfriswmgr  30438  1to3vfriendship  30439  2pthfrgrrn  30440  3cyclfrgrrn1  30443  4cycl2v2nb  30447  n4cyclfrgr  30449  frgrnbnb  30451  frgrncvvdeqlem3  30459  frgrncvvdeqlem6  30462  frgrwopregbsn  30475  frgrwopreglem5ALT  30480  fusgr2wsp2nb  30492  2clwwlk2clwwlklem  30504  indpreima  33003  indsupp  33005  pmtrprfv2  33228  cyc3genpmlem  33291  measxun2  34467  measssd  34472  revwlk  35435  cusgr3cyclex  35446  2cycl2d  35449  poimirlem9  38088  poimirlem15  38094  dihprrn  42010  dvh3dim  42030  dvh3dim3N  42033  lcfrlem21  42147  mapdindp4  42307  mapdh6eN  42324  mapdh7dN  42334  mapdh8ab  42361  mapdh8ad  42363  mapdh8b  42364  mapdh8e  42368  hdmap1l6e  42398  hdmap11lem2  42426  sprsymrelf  48061  paireqne  48077  reuopreuprim  48092  dfodd5  48242  clnbupgrel  48416  clnbgrsym  48420  grtriproplem  48521  grtrif1o  48524  grtriclwlk3  48527  cycl3grtrilem  48528  usgrgrtrirex  48532  isubgr3stgrlem6  48553  isubgr3stgrlem7  48554  grlimprclnbgr  48578  grlimprclnbgrvtx  48581  usgrexmpl2nb1  48614  usgrexmpl2nb2  48615  usgrexmpl2nb3  48616  usgrexmpl2nb4  48617  usgrexmpl2nb5  48618  gpgprismgriedgdmss  48634  gpgedgvtx0  48643  gpgedgvtx1  48644  gpgedg2ov  48648  gpgedg2iv  48649  gpg5nbgrvtx03starlem3  48652  gpg5nbgrvtx03star  48662  gpg5nbgr3star  48663  gpgprismgr4cycllem3  48679  gpgprismgr4cycllem8  48684  pgnbgreunbgrlem1  48695  pgnbgreunbgrlem2lem3  48698  pgnbgreunbgrlem2  48699  pgnbgreunbgrlem4  48701  pgnbgreunbgrlem5  48705  pgnbgreunbgr  48707  pgn4cyclex  48708  glbprlem  49546  toslat  49563