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

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

Proof of Theorem prcom
StepHypRef Expression
1 uncom 3451 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3781 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3781 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2434 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1649    u. cun 3278   {csn 3774   {cpr 3775
This theorem is referenced by:  preq2  3844  tpcoma  3860  tpidm23  3867  prid2g  3871  prid2  3873  prprc2  3875  difprsn2  3896  tpprceq3  3898  tppreqb  3899  preqr2  3933  preq12b  3934  prnebg  3939  fvpr2  5895  fvpr2g  5897  hashprb  11623  joincomALT  14413  meetcomALT  14415  lspprid2  16029  lspexchn2  16158  lspindp2l  16161  lspindp2  16162  lsppratlem1  16174  usgraedgprv  21349  usgraedgrnv  21350  usgra2edg  21355  usgraedg4  21359  usgraidx2vlem1  21363  usgraidx2vlem2  21364  nbgraeledg  21395  nbgrasym  21402  nbgracnvfv  21403  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem1  21413  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgra2v  21424  cusgra3v  21426  uvtxnbgra  21455  2trllemH  21505  2trllemE  21506  wlkntrllem2  21513  usgrcyclnl2  21581  4cycl4dv  21607  cusconngra  21616  vdgr1c  21629  vdegp1ci  21661  indf  24366  indpreima  24375  measxun2  24517  measssd  24522  uvcvvcl  27104  en2other2  27250  symggen  27279  psgnghm  27305  usgra2pthlem1  28040  frgraunss  28099  frisusgranb  28101  frgra3v  28106  3vfriswmgra  28109  1to3vfriswmgra  28111  1to3vfriendship  28112  2pthfrgrarn  28113  2pthfrgra  28115  3cyclfrgrarn1  28116  4cycl2v2nb  28120  n4cyclfrgra  28122  frgranbnb  28124  frgrancvvdeqlem2  28134  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrawopreglem4  28150  frgrawopreg  28152  frgrawopreg2  28154  frg2woteqm  28162  usg2spot2nb  28168  dihprrn  31909  dvh3dim  31929  dvh3dim3N  31932  lcfrlem21  32046  mapdindp4  32206  mapdh6eN  32223  mapdh7dN  32233  mapdh8ab  32260  mapdh8ad  32262  mapdh8b  32263  mapdh8e  32267  hdmap1l6e  32298  hdmap11lem2  32328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-pr 3781
  Copyright terms: Public domain W3C validator