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

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

Proof of Theorem prcom
StepHypRef Expression
1 uncom 4133 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 4567 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 4567 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2859 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cun 3938  {csn 4564  {cpr 4566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-pr 4567
This theorem is referenced by:  preq2  4669  tpcoma  4685  tpidm23  4692  prid2g  4696  prid2  4698  prprc2  4701  difprsn2  4733  tpprceq3  4736  tppreqb  4737  ssprsseq  4757  preq2b  4777  preqr2  4779  preq12b  4780  prnebg  4785  preq12nebg  4792  opthprneg  4794  elpreqpr  4796  elpr2elpr  4798  fvpr2  6951  fvpr2g  6953  en2other2  9429  hashprb  13753  joincomALT  17634  meetcomALT  17636  symggen  18534  psgnran  18579  lspprid2  19706  lspexchn2  19839  lspindp2l  19842  lspindp2  19843  lsppratlem1  19855  psgnghm  20659  uvcvvcl  20866  mdetralt  21152  mdetunilem7  21162  uhgr2edg  26923  usgredg4  26932  usgredg2vlem1  26940  usgredg2vlem2  26941  nbupgrel  27060  nbgr2vtx1edg  27065  nbuhgr2vtx1edgblem  27066  nbuhgr2vtx1edgb  27067  nbusgreledg  27068  nbgrssvwo2  27077  nbgrsym  27078  usgrnbcnvfv  27080  edgnbusgreu  27082  nbusgrf1o0  27084  nb3grprlem1  27095  nb3grprlem2  27096  nb3grpr  27097  nb3grpr2  27098  nb3gr2nb  27099  isuvtx  27110  cusgredg  27139  usgredgsscusgredg  27174  1hegrvtxdg1r  27223  1egrvtxdg1r  27225  vdegp1ci  27253  usgr2wlkneq  27470  usgr2trlncl  27474  usgr2pthlem  27477  uspgrn2crct  27519  2wlkdlem6  27643  umgr2adedgspth  27660  wwlks2onsym  27670  clwwlkn2  27755  clwwlknonex2  27821  wlk2v2elem2  27868  uhgr3cyclexlem  27893  umgr3cyclex  27895  frcond1  27978  frcond3  27981  frgr3v  27987  3vfriswmgr  27990  1to3vfriswmgr  27992  1to3vfriendship  27993  2pthfrgrrn  27994  3cyclfrgrrn1  27997  4cycl2v2nb  28001  n4cyclfrgr  28003  frgrnbnb  28005  frgrncvvdeqlem3  28013  frgrncvvdeqlem6  28016  frgrwopregbsn  28029  frgrwopreglem5ALT  28034  fusgr2wsp2nb  28046  2clwwlk2clwwlklem  28058  pmtrprfv2  30665  cyc3genpmlem  30726  indf  31179  indpreima  31189  measxun2  31374  measssd  31379  revwlk  32274  cusgr3cyclex  32286  2cycl2d  32289  poimirlem9  34787  poimirlem15  34793  dihprrn  38448  dvh3dim  38468  dvh3dim3N  38471  lcfrlem21  38585  mapdindp4  38745  mapdh6eN  38762  mapdh7dN  38772  mapdh8ab  38799  mapdh8ad  38801  mapdh8b  38802  mapdh8e  38806  hdmap1l6e  38836  hdmap11lem2  38864  sprsymrelf  43508  paireqne  43524  reuopreuprim  43539  dfodd5  43676
  Copyright terms: Public domain W3C validator