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

Theorem prcom 4093
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 3633 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 4017 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 4017 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2482 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    u. cun 3459   {csn 4014   {cpr 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-pr 4017
This theorem is referenced by:  preq2  4095  tpcoma  4111  tpidm23  4118  prid2g  4122  prid2  4124  prprc2  4126  difprsn2  4152  tpprceq3  4155  tppreqb  4156  preqr2  4190  preq12b  4191  prnebg  4197  fvpr2  6100  fvpr2g  6102  en2other2  8390  hashprb  12441  joincomALT  15533  meetcomALT  15535  symggen  16369  psgnran  16414  lspprid2  17518  lspexchn2  17651  lspindp2l  17654  lspindp2  17655  lsppratlem1  17667  psgnghm  18489  uvcvvcl  18691  mdetralt  18983  mdetunilem7  18993  usgraedgprv  24248  usgraedgrnv  24249  usgra2edg  24254  usgraedg4  24259  usgraidx2vlem1  24263  usgraidx2vlem2  24264  nbgraeledg  24302  nbgrassvwo2  24310  nbgrasym  24311  nbgracnvfv  24312  nbgraf1olem3  24315  nbgraf1olem5  24317  nb3graprlem1  24323  nb3graprlem2  24324  nb3grapr  24325  nb3grapr2  24326  nb3gra2nb  24327  cusgra2v  24334  cusgra3v  24336  uvtxnbgra  24365  uvtxnb  24369  2trllemH  24426  2trllemE  24427  wlkntrllem2  24434  usgrcyclnl2  24513  4cycl4dv  24539  cusconngra  24548  clwwlkn2  24647  vdgr1c  24777  vdegp1ci  24858  frgraunss  24867  frisusgranb  24869  frgra3v  24874  3vfriswmgra  24877  1to3vfriswmgra  24879  1to3vfriendship  24880  2pthfrgrarn  24881  2pthfrgra  24883  3cyclfrgrarn1  24884  4cycl2v2nb  24888  n4cyclfrgra  24890  frgranbnb  24892  frgrancvvdeqlem2  24903  frgrancvvdeqlem4  24905  frgrancvvdeqlem7  24908  frgrawopreglem4  24919  frgrawopreg  24921  frgrawopreg2  24923  frg2woteqm  24931  usg2spot2nb  24937  numclwwlkovf2ex  24958  indf  27902  indpreima  27911  measxun2  28054  measssd  28059  usgra2pthlem1  32191  usgvincvad  32242  usgvincvadALT  32245  usgedgvadf1lem1  32251  usgedgvadf1lem2  32252  usgedgvadf1ALTlem1  32254  usgedgvadf1ALTlem2  32255  dihprrn  36893  dvh3dim  36913  dvh3dim3N  36916  lcfrlem21  37030  mapdindp4  37190  mapdh6eN  37207  mapdh7dN  37217  mapdh8ab  37244  mapdh8ad  37246  mapdh8b  37247  mapdh8e  37251  hdmap1l6e  37282  hdmap11lem2  37312
  Copyright terms: Public domain W3C validator