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

Theorem prcom 4081
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 3616 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 4005 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 4005 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2468 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3440   {csn 4002   {cpr 4004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-pr 4005
This theorem is referenced by:  preq2  4083  tpcoma  4099  tpidm23  4106  prid2g  4110  prid2  4112  prprc2  4114  difprsn2  4140  tpprceq3  4143  tppreqb  4144  preqr2  4178  preq12b  4179  prnebg  4185  fvpr2  6123  fvpr2g  6125  en2other2  8439  hashprb  12571  joincomALT  16226  meetcomALT  16228  symggen  17062  psgnran  17107  lspprid2  18156  lspexchn2  18289  lspindp2l  18292  lspindp2  18293  lsppratlem1  18305  psgnghm  19079  uvcvvcl  19276  mdetralt  19564  mdetunilem7  19574  usgraedgprv  24949  usgraedgrnv  24950  usgra2edg  24955  usgraedg4  24960  usgraidx2vlem1  24964  usgraidx2vlem2  24965  nbgraeledg  25003  nbgrassvwo2  25011  nbgrasym  25012  nbgracnvfv  25013  nbgraf1olem3  25016  nbgraf1olem5  25018  nb3graprlem1  25024  nb3graprlem2  25025  nb3grapr  25026  nb3grapr2  25027  nb3gra2nb  25028  cusgra2v  25035  cusgra3v  25037  uvtxnbgra  25066  uvtxnb  25070  2trllemH  25127  2trllemE  25128  wlkntrllem2  25135  usgrcyclnl2  25214  4cycl4dv  25240  cusconngra  25249  clwwlkn2  25348  vdgr1c  25478  vdegp1ci  25559  frgraunss  25568  frisusgranb  25570  frgra3v  25575  3vfriswmgra  25578  1to3vfriswmgra  25580  1to3vfriendship  25581  2pthfrgrarn  25582  2pthfrgra  25584  3cyclfrgrarn1  25585  4cycl2v2nb  25589  n4cyclfrgra  25591  frgranbnb  25593  frgrancvvdeqlem2  25604  frgrancvvdeqlem4  25606  frgrancvvdeqlem7  25609  frgrawopreglem4  25620  frgrawopreg  25622  frgrawopreg2  25624  frg2woteqm  25632  usg2spot2nb  25638  numclwwlkovf2ex  25659  pmtrprfv2  28450  indf  28676  indpreima  28685  measxun2  28871  measssd  28876  poimirlem9  31653  poimirlem15  31659  dihprrn  34703  dvh3dim  34723  dvh3dim3N  34726  lcfrlem21  34840  mapdindp4  35000  mapdh6eN  35017  mapdh7dN  35027  mapdh8ab  35054  mapdh8ad  35056  mapdh8b  35057  mapdh8e  35061  hdmap1l6e  35092  hdmap11lem2  35122  dfodd5  38179  usgra2pthlem1  38423  usgvincvad  38474  usgvincvadALT  38477  usgedgvadf1lem1  38483  usgedgvadf1lem2  38484  usgedgvadf1ALTlem1  38486  usgedgvadf1ALTlem2  38487
  Copyright terms: Public domain W3C validator