Theorem prcom 4695

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152  {csn 4588  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-pr 4591

This theorem is used by:  preq2  4697  tpcoma  4713  tpidm23  4720  prid2g  4724  prid2  4726  prprc2  4729  difprsn2  4766  tpprceq3  4769  tppreqb  4770  ssprsseq  4786  preq2b  4807  preqr2  4809  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpreqpr  4827  elpr2elpr  4829  fvpr2g  7227  en2other2  10127  indf  12366  hashprb  14582  joincomALT  18623  meetcomALT  18625  symggen  19735  psgnran  19780  lspprid2  21324  lspexchn2  21460  lspindp2l  21463  lspindp2  21464  lsppratlem1  21476  psgnghm  21941  uvcvvcl  22148  mdetralt  22978  mdetunilem7  22988  uhgr2edg  29846  usgredg4  29855  usgredg2vlem1  29863  usgredg2vlem2  29864  nbupgrel  29983  nbgr2vtx1edg  29988  nbuhgr2vtx1edgblem  29989  nbuhgr2vtx1edgb  29990  nbusgreledg  29991  nbgrssvwo2  30000  nbgrsym  30001  usgrnbcnvfv  30003  edgnbusgreu  30005  nbusgrf1o0  30007  nb3grprlem1  30018  nb3grprlem2  30019  nb3grpr  30020  nb3grpr2  30021  nb3gr2nb  30022  isuvtx  30033  cusgredg  30062  usgredgsscusgredg  30097  1hegrvtxdg1r  30146  1egrvtxdg1r  30148  vdegp1ci  30176  revwlk  30324  usgr2wlkneq  30399  usgr2trlncl  30403  usgr2pthlem  30406  uspgrn2crct  30454  2wlkdlem6  30577  umgr2adedgspth  30594  wwlks2onsym  30606  clwwlkn2  30692  clwwlknonex2  30757  umgr2cycllem  30803  wlk2v2elem2  30814  uhgr3cyclexlem  30839  umgr3cyclex  30841  frcond1  30924  frcond3  30927  frgr3v  30933  3vfriswmgr  30936  1to3vfriswmgr  30938  1to3vfriendship  30939  2pthfrgrrn  30940  3cyclfrgrrn1  30943  4cycl2v2nb  30947  n4cyclfrgr  30949  frgrnbnb  30951  frgrncvvdeqlem3  30959  frgrncvvdeqlem6  30962  frgrwopregbsn  30975  frgrwopreglem5ALT  30980  fusgr2wsp2nb  30992  2clwwlk2clwwlklem  31004  indpreima  33528  indsupp  33530  pmtrprfv2  33748  cyc3genpmlem  33811  measxun2  34954  measssd  34959  cusgr3cyclex  36109  2cycl2d  36110  poimirlem9  38815  poimirlem15  38821  dihprrn  42749  dvh3dim  42769  dvh3dim3N  42772  lcfrlem21  42886  mapdindp4  43046  mapdh6eN  43063  mapdh7dN  43073  mapdh8ab  43100  mapdh8ad  43102  mapdh8b  43103  mapdh8e  43107  hdmap1l6e  43137  hdmap11lem2  43165  sprsymrelf  48850  paireqne  48866  reuopreuprim  48881  dfodd5  49031  clnbupgrel  49205  clnbgrsym  49209  grtriproplem  49310  grtrif1o  49313  grtriclwlk3  49316  cycl3grtrilem  49317  usgrgrtrirex  49321  isubgr3stgrlem6  49342  isubgr3stgrlem7  49343  grlimprclnbgr  49367  grlimprclnbgrvtx  49370  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  gpgprismgriedgdmss  49423  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgedg2ov  49437  gpgedg2iv  49438  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx03star  49451  gpg5nbgr3star  49452  gpgprismgr4cycllem3  49468  gpgprismgr4cycllem8  49473  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5  49494  pgnbgreunbgr  49496  pgn4cyclex  49497  glbprlem  50410  toslat  50427