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

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

Proof of Theorem prcom
StepHypRef Expression
1 uncom 4118 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 4594 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 4594 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2775 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cun 3913  {csn 4591  {cpr 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-pr 4594
This theorem is referenced by:  preq2  4700  tpcoma  4716  tpidm23  4723  prid2g  4727  prid2  4729  prprc2  4732  difprsn2  4766  tpprceq3  4769  tppreqb  4770  ssprsseq  4790  preq2b  4810  preqr2  4812  preq12b  4813  prnebg  4818  preq12nebg  4825  opthprneg  4827  elpreqpr  4829  elpr2elpr  4831  fvpr2g  7142  fvpr2gOLD  7143  fvpr2OLD  7147  en2other2  9952  hashprb  14304  joincomALT  18297  meetcomALT  18299  symggen  19259  psgnran  19304  lspprid2  20475  lspexchn2  20608  lspindp2l  20611  lspindp2  20612  lsppratlem1  20624  psgnghm  21000  uvcvvcl  21209  mdetralt  21973  mdetunilem7  21983  uhgr2edg  28198  usgredg4  28207  usgredg2vlem1  28215  usgredg2vlem2  28216  nbupgrel  28335  nbgr2vtx1edg  28340  nbuhgr2vtx1edgblem  28341  nbuhgr2vtx1edgb  28342  nbusgreledg  28343  nbgrssvwo2  28352  nbgrsym  28353  usgrnbcnvfv  28355  edgnbusgreu  28357  nbusgrf1o0  28359  nb3grprlem1  28370  nb3grprlem2  28371  nb3grpr  28372  nb3grpr2  28373  nb3gr2nb  28374  isuvtx  28385  cusgredg  28414  usgredgsscusgredg  28449  1hegrvtxdg1r  28498  1egrvtxdg1r  28500  vdegp1ci  28528  usgr2wlkneq  28746  usgr2trlncl  28750  usgr2pthlem  28753  uspgrn2crct  28795  2wlkdlem6  28918  umgr2adedgspth  28935  wwlks2onsym  28945  clwwlkn2  29030  clwwlknonex2  29095  wlk2v2elem2  29142  uhgr3cyclexlem  29167  umgr3cyclex  29169  frcond1  29252  frcond3  29255  frgr3v  29261  3vfriswmgr  29264  1to3vfriswmgr  29266  1to3vfriendship  29267  2pthfrgrrn  29268  3cyclfrgrrn1  29271  4cycl2v2nb  29275  n4cyclfrgr  29277  frgrnbnb  29279  frgrncvvdeqlem3  29287  frgrncvvdeqlem6  29290  frgrwopregbsn  29303  frgrwopreglem5ALT  29308  fusgr2wsp2nb  29320  2clwwlk2clwwlklem  29332  pmtrprfv2  31981  cyc3genpmlem  32042  indf  32654  indpreima  32664  measxun2  32849  measssd  32854  revwlk  33758  cusgr3cyclex  33770  2cycl2d  33773  poimirlem9  36116  poimirlem15  36122  dihprrn  39918  dvh3dim  39938  dvh3dim3N  39941  lcfrlem21  40055  mapdindp4  40215  mapdh6eN  40232  mapdh7dN  40242  mapdh8ab  40269  mapdh8ad  40271  mapdh8b  40272  mapdh8e  40276  hdmap1l6e  40306  hdmap11lem2  40334  sprsymrelf  45761  paireqne  45777  reuopreuprim  45792  dfodd5  45926  glbprlem  47072  toslat  47081
  Copyright terms: Public domain W3C validator