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

Theorem prcom 4060
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 3607 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3987 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3987 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2493 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    u. cun 3433   {csn 3984   {cpr 3986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-un 3440  df-pr 3987
This theorem is referenced by:  preq2  4062  tpcoma  4078  tpidm23  4085  prid2g  4089  prid2  4091  prprc2  4093  difprsn2  4118  tpprceq3  4120  tppreqb  4121  preqr2  4154  preq12b  4155  prnebg  4161  fvpr2  6030  fvpr2g  6032  en2other2  8286  hashprb  12274  joincomALT  15317  meetcomALT  15319  symggen  16094  psgnran  16139  lspprid2  17201  lspexchn2  17334  lspindp2l  17337  lspindp2  17338  lsppratlem1  17350  psgnghm  18134  uvcvvcl  18336  mdetralt  18545  mdetunilem7  18555  usgraedgprv  23446  usgraedgrnv  23447  usgra2edg  23452  usgraedg4  23456  usgraidx2vlem1  23460  usgraidx2vlem2  23461  nbgraeledg  23492  nbgrasym  23499  nbgracnvfv  23500  nbgraf1olem3  23503  nbgraf1olem5  23505  nb3graprlem1  23510  nb3graprlem2  23511  nb3grapr  23512  nb3grapr2  23513  nb3gra2nb  23514  cusgra2v  23521  cusgra3v  23523  uvtxnbgra  23552  2trllemH  23602  2trllemE  23603  wlkntrllem2  23610  usgrcyclnl2  23678  4cycl4dv  23704  cusconngra  23713  vdgr1c  23726  vdegp1ci  23758  indf  26616  indpreima  26625  measxun2  26768  measssd  26773  nbgrassvwo2  30424  uvtxnb  30425  usgra2pthlem1  30447  clwwlkn2  30585  frgraunss  30734  frisusgranb  30736  frgra3v  30741  3vfriswmgra  30744  1to3vfriswmgra  30746  1to3vfriendship  30747  2pthfrgrarn  30748  2pthfrgra  30750  3cyclfrgrarn1  30751  4cycl2v2nb  30755  n4cyclfrgra  30757  frgranbnb  30759  frgrancvvdeqlem2  30771  frgrancvvdeqlem4  30773  frgrancvvdeqlem7  30776  frgrawopreglem4  30787  frgrawopreg  30789  frgrawopreg2  30791  frg2woteqm  30799  usg2spot2nb  30805  numclwwlkovf2ex  30826  dihprrn  35394  dvh3dim  35414  dvh3dim3N  35417  lcfrlem21  35531  mapdindp4  35691  mapdh6eN  35708  mapdh7dN  35718  mapdh8ab  35745  mapdh8ad  35747  mapdh8b  35748  mapdh8e  35752  hdmap1l6e  35783  hdmap11lem2  35813
  Copyright terms: Public domain W3C validator