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

Theorem prcom 3705
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 3319 . 2  |-  ( { A }  u.  { B } )  =  ( { B }  u.  { A } )
2 df-pr 3647 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
3 df-pr 3647 . 2  |-  { B ,  A }  =  ( { B }  u.  { A } )
41, 2, 33eqtr4i 2313 1  |-  { A ,  B }  =  { B ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1623    u. cun 3150   {csn 3640   {cpr 3641
This theorem is referenced by:  preq2  3707  tpcoma  3723  tpidm23  3730  prid2g  3733  prid2  3735  prprc2  3737  preqr2  3787  preq12b  3788  fvpr2  5723  joincomALT  14135  meetcomALT  14137  lspprid2  15755  lspexchn2  15884  lspindp2l  15887  lspindp2  15888  lsppratlem1  15900  measxun2  23538  measssd  23543  indf  23599  indpreima  23608  vdgr1c  23896  vdegp1ci  23910  nfwpr4c  25285  tolat  25286  uvcvvcl  27236  en2other2  27382  symggen  27411  psgnghm  27437  tpprceq3  28072  usgraedgprv  28122  usgraedgrnv  28123  nbgraeledg  28145  nbgrasym  28152  cusgra2v  28158  uvtxnbgra  28165  frgra2v  28177  frgra3v  28180  3vfriswmgra  28183  1to3vfriswmgra  28185  1to3vfriendship  28186  dihprrn  31616  dvh3dim  31636  dvh3dim3N  31639  lcfrlem21  31753  mapdindp4  31913  mapdh6eN  31930  mapdh7dN  31940  mapdh8ab  31967  mapdh8ad  31969  mapdh8b  31970  mapdh8e  31974  hdmap1l6e  32005  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-pr 3647
  Copyright terms: Public domain W3C validator