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

Theorem prcom 4105
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 3648 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 4030 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 4030 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2506 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    u. cun 3474   {csn 4027   {cpr 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-pr 4030
This theorem is referenced by:  preq2  4107  tpcoma  4123  tpidm23  4130  prid2g  4134  prid2  4136  prprc2  4138  difprsn2  4164  tpprceq3  4167  tppreqb  4168  preqr2  4201  preq12b  4202  prnebg  4208  fvpr2  6103  fvpr2g  6105  en2other2  8383  hashprb  12426  joincomALT  15512  meetcomALT  15514  symggen  16291  psgnran  16336  lspprid2  17427  lspexchn2  17560  lspindp2l  17563  lspindp2  17564  lsppratlem1  17576  psgnghm  18383  uvcvvcl  18585  mdetralt  18877  mdetunilem7  18887  usgraedgprv  24052  usgraedgrnv  24053  usgra2edg  24058  usgraedg4  24063  usgraidx2vlem1  24067  usgraidx2vlem2  24068  nbgraeledg  24106  nbgrassvwo2  24114  nbgrasym  24115  nbgracnvfv  24116  nbgraf1olem3  24119  nbgraf1olem5  24121  nb3graprlem1  24127  nb3graprlem2  24128  nb3grapr  24129  nb3grapr2  24130  nb3gra2nb  24131  cusgra2v  24138  cusgra3v  24140  uvtxnbgra  24169  uvtxnb  24173  2trllemH  24230  2trllemE  24231  wlkntrllem2  24238  usgrcyclnl2  24317  4cycl4dv  24343  cusconngra  24352  clwwlkn2  24451  vdgr1c  24581  vdegp1ci  24662  frgraunss  24671  frisusgranb  24673  frgra3v  24678  3vfriswmgra  24681  1to3vfriswmgra  24683  1to3vfriendship  24684  2pthfrgrarn  24685  2pthfrgra  24687  3cyclfrgrarn1  24688  4cycl2v2nb  24692  n4cyclfrgra  24694  frgranbnb  24696  frgrancvvdeqlem2  24708  frgrancvvdeqlem4  24710  frgrancvvdeqlem7  24713  frgrawopreglem4  24724  frgrawopreg  24726  frgrawopreg2  24728  frg2woteqm  24736  usg2spot2nb  24742  numclwwlkovf2ex  24763  indf  27669  indpreima  27678  measxun2  27821  measssd  27826  usgra2pthlem1  31822  usgvincvad  31873  usgvincvadALT  31876  usgedgvadf1lem1  31882  usgedgvadf1lem2  31883  usgedgvadf1ALTlem1  31885  usgedgvadf1ALTlem2  31886  dihprrn  36223  dvh3dim  36243  dvh3dim3N  36246  lcfrlem21  36360  mapdindp4  36520  mapdh6eN  36537  mapdh7dN  36547  mapdh8ab  36574  mapdh8ad  36576  mapdh8b  36577  mapdh8e  36581  hdmap1l6e  36612  hdmap11lem2  36642
  Copyright terms: Public domain W3C validator