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

Theorem sneq 3611
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 2265 . . 3  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21abbidv 2370 . 2  |-  ( A  =  B  ->  { x  |  x  =  A }  =  { x  |  x  =  B } )
3 df-sn 3606 . 2  |-  { A }  =  { x  |  x  =  A }
4 df-sn 3606 . 2  |-  { B }  =  { x  |  x  =  B }
52, 3, 43eqtr4g 2313 1  |-  ( A  =  B  ->  { A }  =  { B } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619   {cab 2242   {csn 3600
This theorem is referenced by:  sneqi  3612  sneqd  3613  euabsn  3659  absneu  3661  preq1  3666  tpeq3  3677  snssg  3714  sneqrg  3742  sneqbg  3743  opeq1  3756  unisng  3804  opthwiener  4226  suceq  4415  snnex  4482  opeliunxp  4714  relop  4808  elimasng  5013  dmsnsnsn  5124  elxp4  5133  elxp5  5134  fconstg  5352  f1osng  5438  fveq2  5444  fsng  5617  fnressn  5625  fressnfv  5627  funfvima3  5675  isofrlem  5757  isoselem  5758  1stval  6044  2ndval  6045  2ndval2  6058  fo1st  6059  fo2nd  6060  f1stres  6061  f2ndres  6062  mpt2mptsx  6107  dmmpt2ssx  6109  fmpt2x  6110  ovmptss  6120  fparlem3  6140  fparlem4  6141  brtpos2  6160  dftpos4  6173  tpostpos  6174  iotajust  6210  opabiotafun  6243  eceq1  6650  fvdiagfn  6766  mapsncnv  6768  elixpsn  6809  ixpsnf1o  6810  ensn1g  6880  en1  6882  difsnen  6898  xpsneng  6901  xpcomco  6906  xpassen  6910  xpdom2  6911  canth2  6968  phplem3  6996  xpfi  7082  marypha2lem2  7143  cardsn  7556  pm54.43  7587  dfac5lem3  7706  dfac5lem4  7707  kmlem9  7738  kmlem11  7740  kmlem12  7741  ackbij1lem8  7807  r1om  7824  fictb  7825  hsmexlem4  8009  axcc2lem  8016  axcc2  8017  axdc3lem4  8033  fpwwe2cbv  8206  fpwwe2lem3  8209  fpwwecbv  8220  canth4  8223  fsum2dlem  12184  fsumcnv  12187  fsumcom2  12188  ackbijnn  12237  xpnnenOLD  12436  vdwlem1  12976  vdwlem12  12987  vdwlem13  12988  vdwnn  12993  0ram  13015  ramz2  13019  pwsval  13333  xpsfval  13417  xpsval  13422  sylow2a  14878  efgrelexlema  15006  gsum2d  15171  gsum2d2  15173  gsumcom2  15174  dprdcntz  15191  dprddisj  15192  dprd2dlem2  15223  dprd2dlem1  15224  dprd2da  15225  ablfac1eu  15256  ablfaclem3  15270  lssats2  15705  lspsneq0  15717  lbsind  15781  lspsneq  15823  lspdisj2  15828  lspsnsubn0  15841  lspprat  15854  islbs2  15855  lbsextlem4  15862  lbsextg  15863  lpi0  15947  lpi1  15948  psrvsca  16084  coe1fv  16235  coe1tm  16297  islp  16820  perfi  16834  t1sncld  17002  dis2ndc  17134  nllyi  17149  ptbasfi  17224  txkgen  17294  xkofvcn  17326  xkoinjcn  17329  qtopeu  17355  txswaphmeolem  17443  pt1hmeo  17445  elflim2  17607  tsmsxplem1  17783  tsmsxplem2  17784  itg11  18994  i1faddlem  18996  i1fmullem  18997  itg1addlem3  19001  itg1mulc  19007  eldv  19196  evlssca  19354  mpfind  19376  pf1ind  19386  ply1lpir  19512  areambl  20201  gxval  20871  h1de2ctlem  22080  spansn  22084  elspansn  22091  elspansn2  22092  spansneleq  22095  h1datom  22107  spansnj  22190  spansncv  22196  superpos  22880  sumdmdlem2  22945  cvmscbv  23147  cvmsdisj  23159  cvmsss2  23163  cvmliftlem15  23187  cvmlift2lem11  23202  cvmlift2lem12  23203  cvmlift2lem13  23204  vdgrval  23248  predeq3  23526  fvsingle  23820  snelsingles  23822  dfiota3  23823  brapply  23838  funpartfv  23844  altopeq12  23857  ranksng  24158  fatesg  24308  snelpwg  24443  cbicp  24519  valcurfn1  24557  osneisi  24884  islimrs  24933  isder  25060  valtar  25236  lineval222  25432  lineval3a  25436  sgplpte21  25485  sgplpte22  25491  isray2  25506  isray  25507  neibastop3  25664  tailval  25675  filnetlem4  25683  heiborlem3  25890  ismrer1  25915  mzpclval  26156  mzpcl1  26160  wopprc  26476  inisegn0  26493  dnnumch3lem  26496  aomclem8  26512  frlmlbs  26602  mapfien2  26611  lindfind  26639  lindsind  26640  lindfrn  26644  pmtrfv  26748  mendvsca  26852  cytpval  26881  dvconstbi  26904  bnj1373  28093  bnj1489  28119  lshpnel2N  28326  lsatlspsn2  28333  lsatlspsn  28334  lsatspn0  28341  lkrscss  28439  lfl1dim  28462  lfl1dim2N  28463  ldualvs  28478  atpointN  29083  watvalN  29333  trnsetN  29496  dih1dimatlem  30670  dihatexv  30679  dihjat1lem  30769  dihjat1  30770  lcfl7N  30842  lcfl8  30843  lcfl9a  30846  lcfrlem8  30890  lcfrlem9  30891  lcf1o  30892  mapdval2N  30971  mapdval4N  30973  mapdspex  31009  mapdn0  31010  mapdpglem23  31035  mapdpg  31047  mapdindp1  31061  mapdheq  31069  hvmapval  31101  mapdh9a  31131  hdmap1eq  31143  hdmap1cbv  31144  hdmapval  31172  hdmap10  31184  hdmaplkr  31257
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 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-sn 3606
  Copyright terms: Public domain W3C validator