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

Theorem sneq 3555
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sneq  |-  ( A  =  B  ->  { A }  =  { B } )

Proof of Theorem sneq
StepHypRef Expression
1 eqeq2 2262 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2363 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3550 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3550 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2310 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619   {cab 2239   {csn 3544
This theorem is referenced by:  sneqi  3556  sneqd  3557  euabsn  3603  absneu  3605  preq1  3610  tpeq3  3621  snssg  3656  sneqrg  3682  sneqbg  3683  opeq1  3696  unisng  3744  opthwiener  4161  suceq  4350  snnex  4415  opeliunxp  4647  relop  4741  elimasng  4946  dmsnsnsn  5057  elxp4  5066  elxp5  5067  fconstg  5285  f1osng  5371  fveq2  5377  fsng  5549  fnressn  5557  fressnfv  5559  funfvima3  5607  isofrlem  5689  isoselem  5690  1stval  5976  2ndval  5977  2ndval2  5990  fo1st  5991  fo2nd  5992  f1stres  5993  f2ndres  5994  mpt2mptsx  6039  dmmpt2ssx  6041  fmpt2x  6042  ovmptss  6052  fparlem3  6072  fparlem4  6073  brtpos2  6092  dftpos4  6105  tpostpos  6106  iotajust  6142  opabiotafun  6175  eceq1  6582  fvdiagfn  6698  mapsncnv  6700  elixpsn  6741  ixpsnf1o  6742  ensn1g  6811  en1  6813  difsnen  6829  xpsneng  6832  xpcomco  6837  xpassen  6841  xpdom2  6842  canth2  6899  phplem3  6927  xpfi  7013  marypha2lem2  7073  cardsn  7486  pm54.43  7517  dfac5lem3  7636  dfac5lem4  7637  kmlem9  7668  kmlem11  7670  kmlem12  7671  ackbij1lem8  7737  r1om  7754  fictb  7755  hsmexlem4  7939  axcc2lem  7946  axcc2  7947  axdc3lem4  7963  fpwwe2cbv  8132  fpwwe2lem3  8135  fpwwecbv  8146  canth4  8149  fsum2dlem  12110  fsumcnv  12113  fsumcom2  12114  ackbijnn  12163  xpnnenOLD  12362  vdwlem1  12902  vdwlem12  12913  vdwlem13  12914  vdwnn  12919  0ram  12941  ramz2  12945  pwsval  13259  xpsfval  13343  xpsval  13348  sylow2a  14765  efgrelexlema  14893  gsum2d  15058  gsum2d2  15060  gsumcom2  15061  dprdcntz  15078  dprddisj  15079  dprd2dlem2  15110  dprd2dlem1  15111  dprd2da  15112  ablfac1eu  15143  ablfaclem3  15157  lssats2  15592  lspsneq0  15604  lbsind  15668  lspsneq  15710  lspdisj2  15715  lspsnsubn0  15728  lspprat  15740  islbs2  15741  lbsextlem4  15746  lbsextg  15747  lpi0  15831  lpi1  15832  psrvsca  15968  coe1fv  16119  coe1tm  16181  islp  16704  perfi  16718  t1sncld  16886  dis2ndc  17018  nllyi  17033  ptbasfi  17108  txkgen  17178  xkofvcn  17210  xkoinjcn  17213  qtopeu  17239  txswaphmeolem  17327  pt1hmeo  17329  elflim2  17491  tsmsxplem1  17667  tsmsxplem2  17668  itg11  18878  i1faddlem  18880  i1fmullem  18881  itg1addlem3  18885  itg1mulc  18891  eldv  19080  evlssca  19238  mpfind  19260  pf1ind  19270  ply1lpir  19396  areambl  20085  gxval  20755  h1de2ctlem  21964  spansn  21968  elspansn  21975  elspansn2  21976  spansneleq  21979  h1datom  21991  spansnj  22074  spansncv  22080  superpos  22764  sumdmdlem2  22829  cvmscbv  22960  cvmsdisj  22972  cvmsss2  22976  cvmliftlem15  23000  cvmlift2lem11  23015  cvmlift2lem12  23016  cvmlift2lem13  23017  vdgrval  23061  predeq3  23339  fvsingle  23633  snelsingles  23635  dfiota3  23636  brapply  23651  funpartfv  23657  altopeq12  23670  ranksng  23971  fatesg  24121  snelpwg  24256  cbicp  24332  valcurfn1  24370  osneisi  24697  islimrs  24746  isder  24873  valtar  25049  lineval222  25245  lineval3a  25249  sgplpte21  25298  sgplpte22  25304  isray2  25319  isray  25320  neibastop3  25477  tailval  25488  filnetlem4  25496  heiborlem3  25703  ismrer1  25728  mzpclval  25969  mzpcl1  25973  wopprc  26289  inisegn0  26306  dnnumch3lem  26309  aomclem8  26325  frlmlbs  26415  mapfien2  26424  lindfind  26452  lindsind  26453  lindfrn  26457  pmtrfv  26561  mendvsca  26665  cytpval  26694  dvconstbi  26717  bnj1373  27749  bnj1489  27775  lshpnel2N  27864  lsatlspsn2  27871  lsatlspsn  27872  lsatspn0  27879  lkrscss  27977  lfl1dim  28000  lfl1dim2N  28001  ldualvs  28016  atpointN  28621  watvalN  28871  trnsetN  29034  dih1dimatlem  30208  dihatexv  30217  dihjat1lem  30307  dihjat1  30308  lcfl7N  30380  lcfl8  30381  lcfl9a  30384  lcfrlem8  30428  lcfrlem9  30429  lcf1o  30430  mapdval2N  30509  mapdval4N  30511  mapdspex  30547  mapdn0  30548  mapdpglem23  30573  mapdpg  30585  mapdindp1  30599  mapdheq  30607  hvmapval  30639  mapdh9a  30669  hdmap1eq  30681  hdmap1cbv  30682  hdmapval  30710  hdmap10  30722  hdmaplkr  30795
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-sn 3550
  Copyright terms: Public domain W3C validator