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

Theorem prcom 4094
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 3634 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 4019 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 4019 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2493 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    u. cun 3459   {csn 4016   {cpr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-pr 4019
This theorem is referenced by:  preq2  4096  tpcoma  4112  tpidm23  4119  prid2g  4123  prid2  4125  prprc2  4127  difprsn2  4153  tpprceq3  4156  tppreqb  4157  preqr2  4191  preq12b  4192  prnebg  4198  fvpr2  6091  fvpr2g  6093  en2other2  8378  hashprb  12446  joincomALT  15858  meetcomALT  15860  symggen  16694  psgnran  16739  lspprid2  17839  lspexchn2  17972  lspindp2l  17975  lspindp2  17976  lsppratlem1  17988  psgnghm  18789  uvcvvcl  18989  mdetralt  19277  mdetunilem7  19287  usgraedgprv  24578  usgraedgrnv  24579  usgra2edg  24584  usgraedg4  24589  usgraidx2vlem1  24593  usgraidx2vlem2  24594  nbgraeledg  24632  nbgrassvwo2  24640  nbgrasym  24641  nbgracnvfv  24642  nbgraf1olem3  24645  nbgraf1olem5  24647  nb3graprlem1  24653  nb3graprlem2  24654  nb3grapr  24655  nb3grapr2  24656  nb3gra2nb  24657  cusgra2v  24664  cusgra3v  24666  uvtxnbgra  24695  uvtxnb  24699  2trllemH  24756  2trllemE  24757  wlkntrllem2  24764  usgrcyclnl2  24843  4cycl4dv  24869  cusconngra  24878  clwwlkn2  24977  vdgr1c  25107  vdegp1ci  25188  frgraunss  25197  frisusgranb  25199  frgra3v  25204  3vfriswmgra  25207  1to3vfriswmgra  25209  1to3vfriendship  25210  2pthfrgrarn  25211  2pthfrgra  25213  3cyclfrgrarn1  25214  4cycl2v2nb  25218  n4cyclfrgra  25220  frgranbnb  25222  frgrancvvdeqlem2  25233  frgrancvvdeqlem4  25235  frgrancvvdeqlem7  25238  frgrawopreglem4  25249  frgrawopreg  25251  frgrawopreg2  25253  frg2woteqm  25261  usg2spot2nb  25267  numclwwlkovf2ex  25288  indf  28245  indpreima  28254  measxun2  28418  measssd  28423  dfodd5  32571  usgra2pthlem1  32725  usgvincvad  32776  usgvincvadALT  32779  usgedgvadf1lem1  32785  usgedgvadf1lem2  32786  usgedgvadf1ALTlem1  32788  usgedgvadf1ALTlem2  32789  dihprrn  37550  dvh3dim  37570  dvh3dim3N  37573  lcfrlem21  37687  mapdindp4  37847  mapdh6eN  37864  mapdh7dN  37874  mapdh8ab  37901  mapdh8ad  37903  mapdh8b  37904  mapdh8e  37908  hdmap1l6e  37939  hdmap11lem2  37969
  Copyright terms: Public domain W3C validator