Theorem sneq 4030

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
sneq	|- ( A = B -> { A } = { B } )

Proof of Theorem sneq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2475	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2596	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 4021	. 2 |- { A } = { x | x = A }
4		df-sn 4021	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2526	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1374   {cab 2445   {csn 4020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-sn 4021

This theorem is referenced by:  sneqi  4031  sneqd  4032  euabsn  4092  absneu  4094  preq1  4099  tpeq3  4110  snssg  4153  sneqrg  4189  sneqbg  4190  opeq1  4206  unisng  4254  opthwiener  4742  otiunsndisj  4746  suceq  4936  opeliunxp  5043  relop  5144  elimasng  5354  xpdifid  5426  dmsnsnsn  5477  iotajust  5541  fconstg  5763  f1osng  5845  opabiotafun  5919  fsng  6051  fnressn  6064  fressnfv  6066  funfvima3  6128  f12dfv  6158  f13dfv  6159  isofrlem  6215  isoselem  6216  snnex  6577  elxp4  6718  elxp5  6719  1stval  6776  2ndval  6777  2ndval2  6792  fo1st  6794  fo2nd  6795  f1stres  6796  f2ndres  6797  mpt2mptsx  6837  dmmpt2ssx  6839  fmpt2x  6840  ovmptss  6854  fparlem3  6875  fparlem4  6876  suppval  6893  suppsnop  6905  ressuppssdif  6911  brtpos2  6951  dftpos4  6964  tpostpos  6965  eceq1  7337  fvdiagfn  7453  mapsncnv  7455  elixpsn  7498  ixpsnf1o  7499  ensn1g  7570  en1  7572  difsnen  7589  xpsneng  7592  xpcomco  7597  xpassen  7601  xpdom2  7602  canth2  7660  phplem3  7688  xpfi  7780  marypha2lem2  7885  cardsn  8339  pm54.43  8370  dfac5lem3  8495  dfac5lem4  8496  kmlem9  8527  kmlem11  8529  kmlem12  8530  ackbij1lem8  8596  r1om  8613  fictb  8614  hsmexlem4  8798  axcc2lem  8805  axcc2  8806  axdc3lem4  8822  fpwwe2cbv  8997  fpwwe2lem3  9000  fpwwecbv  9011  canth4  9014  fsum2dlem  13534  fsumcnv  13537  fsumcom2  13538  ackbijnn  13592  xpnnenOLD  13793  vdwlem1  14347  vdwlem12  14358  vdwlem13  14359  vdwnn  14364  0ram  14386  ramz2  14390  pwsval  14730  xpsfval  14811  xpsval  14816  symg2bas  16211  symgfixelsi  16248  pmtrfv  16266  pmtrprfval  16301  sylow2a  16428  efgrelexlema  16556  gsum2dlem2  16782  gsum2dOLD  16784  gsum2d2  16786  gsumcom2  16787  dprdcntz  16825  dprddisj  16826  dprd2dlem2  16872  dprd2dlem1  16873  dprd2da  16874  ablfac1eu  16907  ablfaclem3  16921  lssats2  17422  lspsneq0  17434  lbsind  17502  lspsneq  17544  lspdisj2  17549  lspsnsubn0  17562  lspprat  17575  islbs2  17576  lbsextlem4  17583  lbsextg  17584  lpi0  17670  lpi1  17671  psrvsca  17808  evlssca  17955  mpfind  17969  coe1fv  18009  coe1tm  18078  pf1ind  18155  frlmlbs  18591  lindfind  18611  lindsind  18612  lindfrn  18616  submaval  18843  mdetunilem3  18876  mdetunilem4  18877  mdetunilem9  18882  islp  19400  perfi  19415  t1sncld  19586  bwth  19669  dis2ndc  19720  nllyi  19735  ptbasfi  19810  txkgen  19881  xkofvcn  19913  xkoinjcn  19916  qtopeu  19945  txswaphmeolem  20033  pt1hmeo  20035  elflim2  20193  cnextfvval  20293  cnextcn  20295  cnextfres  20296  tsmsxplem1  20383  tsmsxplem2  20384  ucncn  20516  itg11  21826  i1faddlem  21828  i1fmullem  21829  itg1addlem3  21833  itg1mulc  21839  eldv  22030  ply1lpir  22307  areambl  23009  tglngval  23659  nbgraopALT  24086  nb3graprlem2  24114  cusgrarn  24121  cusgra1v  24123  cusgra2v  24124  cusgra3v  24126  cusgrares  24134  usgrasscusgra  24145  sizeusglecusglem1  24146  uvtxel  24151  cusgrauvtxb  24158  vdgrval  24558  gxval  24786  h1de2ctlem  25999  spansn  26003  elspansn  26010  elspansn2  26011  spansneleq  26014  h1datom  26026  spansnj  26091  spansncv  26097  superpos  26799  sumdmdlem2  26864  dfcnv2  27039  sibfima  27770  sibfof  27772  cvmscbv  28193  cvmsdisj  28205  cvmsss2  28209  cvmliftlem15  28233  cvmlift2lem11  28248  cvmlift2lem12  28249  cvmlift2lem13  28250  fprod2dlem  28537  fprodcnv  28540  fprodcom2  28541  eldm3  28618  elima4  28636  predeq123  28672  fvsingle  28997  snelsingles  28999  dfiota3  29000  brapply  29015  funpartlem  29019  altopeq12  29039  ranksng  29251  neibastop3  29634  tailval  29645  filnetlem4  29653  heiborlem3  29763  ismrer1  29788  mzpclval  30112  mzpcl1  30116  wopprc  30429  inisegn0  30446  dnnumch3lem  30449  aomclem8  30464  mapfien2OLD  30499  mendvsca  30598  cytpval  30627  dvconstbi  30658  fourierdlem32  31258  fourierdlem33  31259  fourierdlem48  31274  usgra2pthlem1  31641  frgraunss  31713  frgra1v  31716  frgra2v  31717  frgra3v  31720  1vwmgra  31721  3vfriswmgra  31723  3cyclfrgrarn1  31730  n4cyclfrgra  31736  frgrancvvdeqlem4  31752  frgrawopreglem4  31766  frgraregorufr0  31771  2spotiundisj  31781  opeliun2xp  31861  dmmpt2ssx2  31865  lindslinindsimp2  32012  ldepspr  32022  ldepsnlinc  32065  bnj1373  33040  bnj1489  33066  lshpnel2N  33657  lsatlspsn2  33664  lsatlspsn  33665  lsatspn0  33672  lkrscss  33770  lfl1dim  33793  lfl1dim2N  33794  ldualvs  33809  atpointN  34414  watvalN  34664  trnsetN  34827  dih1dimatlem  36001  dihatexv  36010  dihjat1lem  36100  dihjat1  36101  lcfl7N  36173  lcfl8  36174  lcfl9a  36177  lcfrlem8  36221  lcfrlem9  36222  lcf1o  36223  mapdval2N  36302  mapdval4N  36304  mapdspex  36340  mapdn0  36341  mapdpglem23  36366  mapdpg  36378  mapdindp1  36392  mapdheq  36400  hvmapval  36432  mapdh9a  36462  hdmap1eq  36474  hdmap1cbv  36475  hdmapval  36503  hdmap10  36515  hdmaplkr  36588