Theorem prcom 4671

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

Syntax hints:   = wceq 1547   ∪ cun 3888  {csn 4562  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-pr 4565

This theorem is referenced by:  preq2  4673  tpcoma  4689  tpidm23  4696  prid2g  4700  prid2  4702  prprc2  4705  difprsn2  4741  tpprceq3  4744  tppreqb  4745  ssprsseq  4763  preq2b  4785  preqr2  4787  preq12b  4788  prnebg  4794  preq12nebg  4801  opthprneg  4803  elpreqpr  4805  elpr2elpr  4807  fvpr2g  7142  en2other2  9929  indf  12163  hashprb  14357  joincomALT  18363  meetcomALT  18365  symggen  19443  psgnran  19488  lspprid2  20995  lspexchn2  21131  lspindp2l  21134  lspindp2  21135  lsppratlem1  21147  psgnghm  21562  uvcvvcl  21769  mdetralt  22598  mdetunilem7  22608  uhgr2edg  29302  usgredg4  29311  usgredg2vlem1  29319  usgredg2vlem2  29320  nbupgrel  29439  nbgr2vtx1edg  29444  nbuhgr2vtx1edgblem  29445  nbuhgr2vtx1edgb  29446  nbusgreledg  29447  nbgrssvwo2  29456  nbgrsym  29457  usgrnbcnvfv  29459  edgnbusgreu  29461  nbusgrf1o0  29463  nb3grprlem1  29474  nb3grprlem2  29475  nb3grpr  29476  nb3grpr2  29477  nb3gr2nb  29478  isuvtx  29489  cusgredg  29518  usgredgsscusgredg  29553  1hegrvtxdg1r  29602  1egrvtxdg1r  29604  vdegp1ci  29632  usgr2wlkneq  29849  usgr2trlncl  29853  usgr2pthlem  29856  uspgrn2crct  29901  2wlkdlem6  30024  umgr2adedgspth  30041  wwlks2onsym  30053  clwwlkn2  30139  clwwlknonex2  30204  wlk2v2elem2  30251  uhgr3cyclexlem  30276  umgr3cyclex  30278  frcond1  30361  frcond3  30364  frgr3v  30370  3vfriswmgr  30373  1to3vfriswmgr  30375  1to3vfriendship  30376  2pthfrgrrn  30377  3cyclfrgrrn1  30380  4cycl2v2nb  30384  n4cyclfrgr  30386  frgrnbnb  30388  frgrncvvdeqlem3  30396  frgrncvvdeqlem6  30399  frgrwopregbsn  30412  frgrwopreglem5ALT  30417  fusgr2wsp2nb  30429  2clwwlk2clwwlklem  30441  indpreima  32951  indsupp  32953  pmtrprfv2  33176  cyc3genpmlem  33239  measxun2  34401  measssd  34406  revwlk  35360  cusgr3cyclex  35371  2cycl2d  35374  poimirlem9  38003  poimirlem15  38009  dihprrn  41925  dvh3dim  41945  dvh3dim3N  41948  lcfrlem21  42062  mapdindp4  42222  mapdh6eN  42239  mapdh7dN  42249  mapdh8ab  42276  mapdh8ad  42278  mapdh8b  42279  mapdh8e  42283  hdmap1l6e  42313  hdmap11lem2  42341  sprsymrelf  47977  paireqne  47993  reuopreuprim  48008  dfodd5  48158  clnbupgrel  48332  clnbgrsym  48336  grtriproplem  48437  grtrif1o  48440  grtriclwlk3  48443  cycl3grtrilem  48444  usgrgrtrirex  48448  isubgr3stgrlem6  48469  isubgr3stgrlem7  48470  grlimprclnbgr  48494  grlimprclnbgrvtx  48497  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  gpgprismgriedgdmss  48550  gpgedgvtx0  48559  gpgedgvtx1  48560  gpgedg2ov  48564  gpgedg2iv  48565  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem8  48600  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  pgnbgreunbgr  48623  pgn4cyclex  48624  glbprlem  49462  toslat  49479