MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prcom Structured version   Visualization version   GIF version

Theorem prcom 4424
Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prcom {𝐴, 𝐵} = {𝐵, 𝐴}

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3921 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 4339 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 4339 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2797 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  cun 3732  {csn 4336  {cpr 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-pr 4339
This theorem is referenced by:  preq2  4426  tpcoma  4442  tpidm23  4449  prid2g  4453  prid2  4455  prprc2  4458  difprsn2  4488  tpprceq3  4491  tppreqb  4492  ssprsseq  4512  preq2b  4532  preqr2  4534  preq12b  4535  prnebg  4542  preq12nebg  4551  opthprneg  4553  elpreqpr  4555  elpr2elpr  4557  fvpr2  6654  fvpr2g  6656  en2other2  9087  hashprb  13391  joincomALT  17309  meetcomALT  17311  symggen  18167  psgnran  18213  lspprid2  19284  lspexchn2  19418  lspindp2l  19421  lspindp2  19422  lsppratlem1  19435  psgnghm  20212  uvcvvcl  20416  mdetralt  20705  mdetunilem7  20715  uhgr2edg  26392  usgredg4  26401  usgredg2vlem1  26409  usgredg2vlem2  26410  nbupgrel  26534  nbgr2vtx1edg  26539  nbuhgr2vtx1edgblem  26540  nbuhgr2vtx1edgb  26541  nbusgreledg  26542  nbgrssvwo2  26551  nbgrssvwo2OLD  26554  nbgrsym  26556  nbgrsymOLD  26557  usgrnbcnvfv  26559  edgnbusgreu  26561  edgnbusgreuOLD  26562  nbusgrf1o0  26564  nb3grprlem1  26575  nb3grprlem2  26576  nb3grpr  26577  nb3grpr2  26578  nb3gr2nb  26579  isuvtx  26592  isuvtxaOLD  26593  cusgredg  26625  usgredgsscusgredg  26660  1hegrvtxdg1r  26709  1egrvtxdg1r  26711  vdegp1ci  26739  usgr2wlkneq  26962  usgr2trlncl  26966  usgr2pthlem  26969  uspgrn2crct  27011  2wlkdlem6  27172  umgr2adedgspth  27189  wwlks2onsym  27200  clwwlkn2  27305  clwwlknonex2  27401  wlk2v2elem2  27452  uhgr3cyclexlem  27477  umgr3cyclex  27479  frcond1  27567  frcond3  27570  frgr3v  27576  3vfriswmgr  27579  1to3vfriswmgr  27581  1to3vfriendship  27582  2pthfrgrrn  27583  3cyclfrgrrn1  27586  4cycl2v2nb  27590  n4cyclfrgr  27592  frgrnbnb  27594  frgrncvvdeqlem3  27602  frgrncvvdeqlem6  27605  frgrwopregbsn  27618  frgrwopreglem5ALT  27623  fusgr2wsp2nb  27635  extwwlkfablem1OLD  27643  2clwwlk2clwwlklem  27652  pmtrprfv2  30316  indf  30545  indpreima  30555  measxun2  30741  measssd  30746  poimirlem9  33863  poimirlem15  33869  dihprrn  37403  dvh3dim  37423  dvh3dim3N  37426  lcfrlem21  37540  mapdindp4  37700  mapdh6eN  37717  mapdh7dN  37727  mapdh8ab  37754  mapdh8ad  37756  mapdh8b  37757  mapdh8e  37761  hdmap1l6e  37791  hdmap11lem2  37819  dfodd5  42272  sprsymrelf  42438
  Copyright terms: Public domain W3C validator