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

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

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3718 . 2 ({𝐴} ∪ {𝐵}) = ({𝐵} ∪ {𝐴})
2 df-pr 4127 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3 df-pr 4127 . 2 {𝐵, 𝐴} = ({𝐵} ∪ {𝐴})
41, 2, 33eqtr4i 2641 1 {𝐴, 𝐵} = {𝐵, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cun 3537  {csn 4124  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-pr 4127
This theorem is referenced by:  preq2  4212  tpcoma  4228  tpidm23  4235  prid2g  4239  prid2  4241  prprc2  4243  difprsn2  4271  tpprceq3  4275  tppreqb  4276  preq2b  4313  preqr2  4316  preq12b  4317  prnebg  4324  elpreqpr  4329  fvpr2  6339  fvpr2g  6341  en2other2  8692  hashprb  13000  joincomALT  16800  meetcomALT  16802  symggen  17661  psgnran  17706  lspprid2  18767  lspexchn2  18900  lspindp2l  18903  lspindp2  18904  lsppratlem1  18916  psgnghm  19692  uvcvvcl  19892  mdetralt  20180  mdetunilem7  20190  usgraedgprv  25698  usgraedgrnv  25699  usgra2edg  25704  usgraedg4  25709  usgraidx2vlem1  25713  usgraidx2vlem2  25714  nbgraeledg  25752  nbgrassvwo2  25760  nbgrasym  25761  nbgracnvfv  25762  nbgraf1olem3  25765  nbgraf1olem5  25767  nb3graprlem1  25773  nb3graprlem2  25774  nb3grapr  25775  nb3grapr2  25776  nb3gra2nb  25777  cusgra2v  25784  cusgra3v  25786  uvtxnbgra  25814  uvtxnb  25818  2trllemH  25875  2trllemE  25876  wlkntrllem2  25883  usgrcyclnl2  25962  4cycl4dv  25988  cusconngra  25997  clwwlkn2  26096  vdgr1c  26225  vdegp1ci  26306  frgraunss  26315  frisusgranb  26317  frgra3v  26322  3vfriswmgra  26325  1to3vfriswmgra  26327  1to3vfriendship  26328  2pthfrgrarn  26329  2pthfrgra  26331  3cyclfrgrarn1  26332  4cycl2v2nb  26336  n4cyclfrgra  26338  frgranbnb  26340  frgrancvvdeqlem2  26351  frgrancvvdeqlem4  26353  frgrancvvdeqlem7  26356  frgrawopreglem4  26367  frgrawopreg  26369  frgrawopreg2  26371  frg2woteqm  26379  usg2spot2nb  26385  numclwwlkovf2ex  26406  pmtrprfv2  28972  indf  29198  indpreima  29207  measxun2  29393  measssd  29398  poimirlem9  32371  poimirlem15  32377  dihprrn  35516  dvh3dim  35536  dvh3dim3N  35539  lcfrlem21  35653  mapdindp4  35813  mapdh6eN  35830  mapdh7dN  35840  mapdh8ab  35867  mapdh8ad  35869  mapdh8b  35870  mapdh8e  35874  hdmap1l6e  35905  hdmap11lem2  35935  dfodd5  39894  ssprsseq  40108  elpr2elpr  40109  uhgr2edg  40416  usgredg4  40425  usgredg2vlem1  40433  usgredg2vlem2  40434  nbupgrel  40548  nbgr2vtx1edg  40553  nbuhgr2vtx1edgblem  40554  nbuhgr2vtx1edgb  40555  nbusgreledg  40556  nbgrssvwo2  40568  nbgrsym  40572  usgrnbcnvfv  40574  edgnbusgreu  40576  nbusgrf1o0  40578  nb3grprlem1  40589  nb3grprlem2  40590  nb3grpr  40591  nb3grpr2  40592  nb3gr2nb  40593  isuvtxa  40602  cusgredg  40627  usgredgsscusgredg  40656  1hegrvtxdg1r  40705  1egrvtxdg1r  40707  vdegp1ci-av  40735  usgr2wlkneq  40943  usgr2trlncl  40947  usgr2pthlem  40950  uspgrn2crct  40992  21wlkdlem6  41119  umgr2adedgspth  41136  clwwlksn2  41198  1wlk2v2elem2  41304  uhgr3cyclexlem  41329  umgr3cyclex  41331  frcond1  41419  frcond3  41421  frgr3v  41426  3vfriswmgr  41429  1to3vfriswmgr  41431  1to3vfriendship-av  41432  2pthfrgrrn  41433  3cyclfrgrrn1  41436  4cycl2v2nb-av  41440  n4cyclfrgr  41442  frgrnbnb  41444  frgrncvvdeqlem2  41451  frgrncvvdeqlem4  41453  frgrncvvdeqlem7  41456  frgrwopreglem4  41465  frgrwopreg  41467  frgrwopreg2  41469  frgr2wwlkeqm  41477  fusgr2wsp2nb  41479  av-extwwlkfablem1  41489  av-numclwwlkovf2ex  41498
  Copyright terms: Public domain W3C validator