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

Theorem prcom 4063
Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
prcom  |-  { A ,  B }  =  { B ,  A }

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3590 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3983 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3983 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2494 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    u. cun 3414   {csn 3980   {cpr 3982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-pr 3983
This theorem is referenced by:  preq2  4065  tpcoma  4081  tpidm23  4088  prid2g  4092  prid2  4094  prprc2  4096  difprsn2  4122  tpprceq3  4125  tppreqb  4126  preq2b  4160  preqr2  4163  preq12b  4164  prnebg  4171  elpreqpr  4175  fvpr2  6137  fvpr2g  6139  en2other2  8471  hashprb  12612  joincomALT  16330  meetcomALT  16332  symggen  17166  psgnran  17211  lspprid2  18276  lspexchn2  18409  lspindp2l  18412  lspindp2  18413  lsppratlem1  18425  psgnghm  19203  uvcvvcl  19400  mdetralt  19688  mdetunilem7  19698  usgraedgprv  25159  usgraedgrnv  25160  usgra2edg  25165  usgraedg4  25170  usgraidx2vlem1  25174  usgraidx2vlem2  25175  nbgraeledg  25214  nbgrassvwo2  25222  nbgrasym  25223  nbgracnvfv  25224  nbgraf1olem3  25227  nbgraf1olem5  25229  nb3graprlem1  25235  nb3graprlem2  25236  nb3grapr  25237  nb3grapr2  25238  nb3gra2nb  25239  cusgra2v  25246  cusgra3v  25248  uvtxnbgra  25277  uvtxnb  25281  2trllemH  25338  2trllemE  25339  wlkntrllem2  25346  usgrcyclnl2  25425  4cycl4dv  25451  cusconngra  25460  clwwlkn2  25559  vdgr1c  25689  vdegp1ci  25770  frgraunss  25779  frisusgranb  25781  frgra3v  25786  3vfriswmgra  25789  1to3vfriswmgra  25791  1to3vfriendship  25792  2pthfrgrarn  25793  2pthfrgra  25795  3cyclfrgrarn1  25796  4cycl2v2nb  25800  n4cyclfrgra  25802  frgranbnb  25804  frgrancvvdeqlem2  25815  frgrancvvdeqlem4  25817  frgrancvvdeqlem7  25820  frgrawopreglem4  25831  frgrawopreg  25833  frgrawopreg2  25835  frg2woteqm  25843  usg2spot2nb  25849  numclwwlkovf2ex  25870  pmtrprfv2  28662  indf  28888  indpreima  28897  measxun2  29083  measssd  29088  poimirlem9  31995  poimirlem15  32001  dihprrn  35040  dvh3dim  35060  dvh3dim3N  35063  lcfrlem21  35177  mapdindp4  35337  mapdh6eN  35354  mapdh7dN  35364  mapdh8ab  35391  mapdh8ad  35393  mapdh8b  35394  mapdh8e  35398  hdmap1l6e  35429  hdmap11lem2  35459  dfodd5  38924  ssprsseq  39139  elpr2elpr  39140  uhgr2edg  39435  usgredg4  39440  usgredg2vlem1  39448  usgredg2vlem2  39449  nbupgrel  39559  nbgr2vtx1edg  39564  nbuhgr2vtx1edgblem  39565  nbuhgr2vtx1edgb  39566  nbusgreledg  39567  nbgrssvwo2  39579  nbgrsym  39583  usgrnbcnvfv  39585  edgnbusgreu  39587  nbusgrf1o0  39589  nb3grprlem1  39600  nb3grprlem2  39601  nb3grpr  39602  nb3grpr2  39603  nb3gr2nb  39604  isuvtxa  39613  cusgredg  39638  usgredgsscusgredg  39666  usgr2wlkneq  39884  uspgrn2crct  39922  1wlk2v2elem2  39967  21wlkdlem6  39976  umgr2adedgspth  39993  uhgr3cyclexlem  40018  umgr3cyclex  40020  usgra2pthlem1  40036  usgvincvad  40085  usgvincvadALT  40088  usgedgvadf1lem1  40094  usgedgvadf1lem2  40095  usgedgvadf1ALTlem1  40097  usgedgvadf1ALTlem2  40098
  Copyright terms: Public domain W3C validator