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

Theorem prcom 3827
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 3436 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3766 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3766 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2419 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1649    u. cun 3263   {csn 3759   {cpr 3760
This theorem is referenced by:  preq2  3829  tpcoma  3845  tpidm23  3852  prid2g  3856  prid2  3858  prprc2  3860  difprsn2  3881  tpprceq3  3883  tppreqb  3884  preqr2  3917  preq12b  3918  prnebg  3923  fvpr2  5877  fvpr2g  5879  hashprb  11597  joincomALT  14387  meetcomALT  14389  lspprid2  16003  lspexchn2  16132  lspindp2l  16135  lspindp2  16136  lsppratlem1  16148  usgraedgprv  21265  usgraedgrnv  21266  usgra2edg  21270  usgraedg4  21274  usgraidx2vlem1  21278  usgraidx2vlem2  21279  nbgraeledg  21310  nbgrasym  21317  nbgracnvfv  21318  nbgraf1olem3  21321  nbgraf1olem5  21323  nb3graprlem1  21328  nb3graprlem2  21329  nb3grapr  21330  nb3grapr2  21331  nb3gra2nb  21332  cusgra2v  21339  cusgra3v  21341  uvtxnbgra  21370  wlkntrllem4  21418  usgrcyclnl2  21478  4cycl4dv  21504  cusconngra  21513  vdgr1c  21526  vdegp1ci  21558  indf  24211  indpreima  24220  measxun2  24360  measssd  24365  uvcvvcl  26907  en2other2  27053  symggen  27082  psgnghm  27108  frgraunss  27750  frisusgranb  27752  frgra3v  27757  3vfriswmgra  27760  1to3vfriswmgra  27762  1to3vfriendship  27763  2pthfrgrarn  27764  2pthfrgra  27766  3cyclfrgrarn1  27767  4cycl2v2nb  27771  n4cyclfrgra  27773  frgranbnb  27775  frgrancvvdeqlem2  27785  frgrancvvdeqlem4  27787  frgrancvvdeqlem7  27790  frgrawopreglem4  27801  frgrawopreg  27803  frgrawopreg2  27805  dihprrn  31543  dvh3dim  31563  dvh3dim3N  31566  lcfrlem21  31680  mapdindp4  31840  mapdh6eN  31857  mapdh7dN  31867  mapdh8ab  31894  mapdh8ad  31896  mapdh8b  31897  mapdh8e  31901  hdmap1l6e  31932  hdmap11lem2  31962
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-un 3270  df-pr 3766
  Copyright terms: Public domain W3C validator