Theorem prcom 4700

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3904  {csn 4591  {cpr 4593

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-pr 4594

This theorem is used by:  preq2  4702  tpcoma  4718  tpidm23  4725  prid2g  4729  prid2  4731  prprc2  4734  difprsn2  4771  tpprceq3  4774  tppreqb  4775  ssprsseq  4793  preq2b  4814  preqr2  4816  preq12b  4817  prnebg  4823  preq12nebg  4830  opthprneg  4832  elpreqpr  4834  elpr2elpr  4836  fvpr2g  7193  en2other2  10005  indf  12235  hashprb  14446  joincomALT  18472  meetcomALT  18474  symggen  19563  psgnran  19608  lspprid2  21148  lspexchn2  21284  lspindp2l  21287  lspindp2  21288  lsppratlem1  21300  psgnghm  21759  uvcvvcl  21966  mdetralt  22794  mdetunilem7  22804  uhgr2edg  29587  usgredg4  29596  usgredg2vlem1  29604  usgredg2vlem2  29605  nbupgrel  29724  nbgr2vtx1edg  29729  nbuhgr2vtx1edgblem  29730  nbuhgr2vtx1edgb  29731  nbusgreledg  29732  nbgrssvwo2  29741  nbgrsym  29742  usgrnbcnvfv  29744  edgnbusgreu  29746  nbusgrf1o0  29748  nb3grprlem1  29759  nb3grprlem2  29760  nb3grpr  29761  nb3grpr2  29762  nb3gr2nb  29763  isuvtx  29774  cusgredg  29803  usgredgsscusgredg  29838  1hegrvtxdg1r  29887  1egrvtxdg1r  29889  vdegp1ci  29917  usgr2wlkneq  30134  usgr2trlncl  30138  usgr2pthlem  30141  uspgrn2crct  30186  2wlkdlem6  30309  umgr2adedgspth  30326  wwlks2onsym  30338  clwwlkn2  30424  clwwlknonex2  30489  wlk2v2elem2  30536  uhgr3cyclexlem  30561  umgr3cyclex  30563  frcond1  30646  frcond3  30649  frgr3v  30655  3vfriswmgr  30658  1to3vfriswmgr  30660  1to3vfriendship  30661  2pthfrgrrn  30662  3cyclfrgrrn1  30665  4cycl2v2nb  30669  n4cyclfrgr  30671  frgrnbnb  30673  frgrncvvdeqlem3  30681  frgrncvvdeqlem6  30684  frgrwopregbsn  30697  frgrwopreglem5ALT  30702  fusgr2wsp2nb  30714  2clwwlk2clwwlklem  30726  indpreima  33214  indsupp  33216  pmtrprfv2  33431  cyc3genpmlem  33494  measxun2  34624  measssd  34629  revwlk  35630  cusgr3cyclex  35641  2cycl2d  35644  poimirlem9  38313  poimirlem15  38319  dihprrn  42233  dvh3dim  42253  dvh3dim3N  42256  lcfrlem21  42370  mapdindp4  42530  mapdh6eN  42547  mapdh7dN  42557  mapdh8ab  42584  mapdh8ad  42586  mapdh8b  42587  mapdh8e  42591  hdmap1l6e  42621  hdmap11lem2  42649  sprsymrelf  48277  paireqne  48293  reuopreuprim  48308  dfodd5  48458  clnbupgrel  48632  clnbgrsym  48636  grtriproplem  48737  grtrif1o  48740  grtriclwlk3  48743  cycl3grtrilem  48744  usgrgrtrirex  48748  isubgr3stgrlem6  48769  isubgr3stgrlem7  48770  grlimprclnbgr  48794  grlimprclnbgrvtx  48797  usgrexmpl2nb1  48830  usgrexmpl2nb2  48831  usgrexmpl2nb3  48832  usgrexmpl2nb4  48833  usgrexmpl2nb5  48834  gpgprismgriedgdmss  48850  gpgedgvtx0  48859  gpgedgvtx1  48860  gpgedg2ov  48864  gpgedg2iv  48865  gpg5nbgrvtx03starlem3  48868  gpg5nbgrvtx03star  48878  gpg5nbgr3star  48879  gpgprismgr4cycllem3  48895  gpgprismgr4cycllem8  48900  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5  48921  pgnbgreunbgr  48923  pgn4cyclex  48924  glbprlem  49776  toslat  49793