Theorem sneq 4631

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

Assertion

Ref	Expression
sneq	⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2736	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2793	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4622	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4622	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1533  {cab 2701  {csn 4621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-sn 4622

This theorem is referenced by:  sneqi  4632  sneqd  4633  euabsn  4723  absneu  4725  preq1  4730  tpeq3  4741  issn  4826  mosneq  4836  sneqbg  4837  opeq1  4866  snexg  5421  propeqop  5498  opthwiener  5505  otiunsndisj  5511  opeliunxp  5734  relop  5841  elimasngOLD  6080  inisegn0  6088  xpdifid  6158  dmsnsnsn  6210  predeq123  6292  suceq  6421  iotajust  6485  iotanul2  6504  fconstg  6769  f1osng  6865  opabiotafun  6963  fvn0ssdmfun  7067  fsng  7128  fsn2g  7129  fnressn  7149  fressnfv  7151  funfvima3  7230  f12dfv  7264  f13dfv  7265  isofrlem  7330  isoselem  7331  elxp4  7907  elxp5  7908  1stval  7971  2ndval  7972  2ndval2  7987  fo1st  7989  fo2nd  7990  f1stres  7993  f2ndres  7994  mpomptsx  8044  dmmpossx  8046  fmpox  8047  ovmptss  8074  fparlem3  8095  fparlem4  8096  xpord2pred  8126  xpord3pred  8133  suppval  8143  suppsnop  8158  ressuppssdif  8165  brtpos2  8213  dftpos4  8226  tpostpos  8227  naddcllem  8672  eceq1  8738  fvdiagfn  8882  mapsncnv  8884  elixpsn  8928  ixpsnf1o  8929  ensn1g  9016  en1  9018  en1OLD  9019  difsnen  9050  xpsneng  9053  xpcomco  9059  xpassen  9063  xpdom2  9064  canth2  9127  rexdif1en  9155  rexdif1enOLD  9156  cnvfi  9177  phplem3OLD  9216  xpfiOLD  9315  marypha2lem2  9428  cardsn  9961  pm54.43  9993  dfac5lem3  10117  dfac5lem4  10118  kmlem9  10150  kmlem11  10152  kmlem12  10153  ackbij1lem8  10219  r1om  10236  fictb  10237  hsmexlem4  10421  axcc2lem  10428  axcc2  10429  axdc3lem4  10445  fpwwe2cbv  10622  fpwwe2lem3  10625  fpwwecbv  10636  canth4  10639  s3iunsndisj  14913  fsum2dlem  15714  fsumcnv  15717  fsumcom2  15718  ackbijnn  15772  fprod2dlem  15922  fprodcnv  15925  fprodcom2  15926  lcmfunsnlem1  16573  lcmfunsnlem2lem1  16574  lcmfunsnlem2lem2  16575  lcmfunsnlem2  16576  lcmfunsn  16580  vdwlem1  16915  vdwlem12  16926  vdwlem13  16927  vdwnn  16932  0ram  16954  ramz2  16958  pwsval  17433  symg2bas  19304  symgfixelsi  19347  pmtrfv  19364  pmtrprfval  19399  sylow2a  19531  efgrelexlema  19661  gsum2dlem2  19883  gsum2d2  19886  gsumcom2  19887  dprdcntz  19922  dprddisj  19923  dprd2dlem2  19954  dprd2dlem1  19955  dprd2da  19956  ablfac1eu  19987  ablfaclem3  20001  lssats2  20839  lspsneq0  20851  lbsind  20920  lspsneq  20965  lspdisj2  20970  lspsnsubn0  20983  lspprat  20996  islbs2  20997  lbsextlem4  21004  lbsextg  21005  lpi0  21171  lpi1  21172  irinitoringc  21336  pzriprnglem13  21350  pzriprnglem14  21351  frlmlbs  21662  lindfind  21681  lindsind  21682  lindfrn  21686  psrvsca  21822  evlssca  21964  mpfind  21982  coe1fv  22050  coe1tm  22116  pf1ind  22198  submaval  22407  mdetunilem3  22440  mdetunilem4  22441  mdetunilem9  22446  islp  22968  perfi  22983  t1sncld  23154  bwth  23238  dis2ndc  23288  nllyi  23303  dissnlocfin  23357  ptbasfi  23409  txkgen  23480  xkofvcn  23512  xkoinjcn  23515  qtopeu  23544  txswaphmeolem  23632  pt1hmeo  23634  elflim2  23792  cnextfvval  23893  cnextcn  23895  cnextfres1  23896  cnextfres  23897  tsmsxplem1  23981  tsmsxplem2  23982  ucncn  24114  itg11  25544  i1faddlem  25546  i1fmullem  25547  itg1addlem3  25551  itg1mulc  25558  eldv  25751  ply1lpir  26038  areambl  26809  conway  27651  scutval  27652  scutcut  27653  scutbday  27656  eqscut  27657  eqscut2  27658  scutun12  27662  scutbdaybnd  27667  scutbdaybnd2  27668  scutbdaylt  27670  bday1s  27683  cuteq0  27684  cuteq1  27685  madebdaylemlrcut  27744  cofcut1  27759  cofcutr  27763  tglngval  28274  edglnl  28875  nbgrval  29065  nbgr2vtx1edg  29079  nbuhgr2vtx1edgb  29081  nbgr1vtx  29087  nb3grprlem2  29110  uvtxel  29117  uvtxel1  29125  uvtxusgrel  29132  cusgredg  29153  cplgr1v  29159  cplgr3v  29164  usgredgsscusgredg  29188  vtxdgval  29197  1loopgrvd2  29232  wlk1walk  29368  wlkres  29399  wlkp1lem8  29409  usgr2pthlem  29492  crctcshwlkn0lem6  29541  2wspiundisj  29689  clwwlknon1  29822  1wlkdlem4  29865  eupth2lem3lem3  29955  frcond1  29991  frgr1v  29996  nfrgr2v  29997  frgr3v  30000  1vwmgr  30001  3vfriswmgr  30003  3cyclfrgrrn1  30010  n4cyclfrgr  30016  frgrwopreglem4a  30035  h1de2ctlem  31280  spansn  31284  elspansn  31291  elspansn2  31292  spansneleq  31295  h1datom  31307  spansnj  31372  spansncv  31378  superpos  32079  sumdmdlem2  32144  aciunf1lem  32359  fnpreimac  32368  dfcnv2  32373  pwrssmgc  32640  gsummpt2co  32671  gsumpart  32678  0nellinds  32955  lindssn  32966  lsmsnidl  32981  nsgmgclem  32994  nsgmgc  32995  nsgqusf1olem1  32996  nsgqusf1olem2  32997  nsgqusf1olem3  32998  pidlnzb  33012  elrspunidl  33018  lbslsat  33183  lindsunlem  33191  extdgval  33215  locfinreflem  33312  esum2dlem  33582  sibfima  33829  sibfof  33831  bnj1373  34532  bnj1489  34558  funen1cnv  34582  fineqvac  34588  cplgredgex  34602  pfxwlk  34605  revwlk  34606  loop1cycl  34619  cvmscbv  34740  cvmsdisj  34752  cvmsss2  34756  cvmliftlem15  34780  cvmlift2lem11  34795  cvmlift2lem12  34796  cvmlift2lem13  34797  satffunlem1lem1  34884  satffunlem2lem1  34886  mvtinf  35037  eldm3  35227  elima4  35243  fvsingle  35388  snelsingles  35390  dfiota3  35391  brapply  35406  funpartlem  35410  altopeq12  35430  ranksng  35635  neibastop3  35738  tailval  35749  filnetlem4  35757  bj-snexg  36406  bj-restsnss  36455  bj-restsnss2  36456  f1omptsnlem  36708  f1omptsn  36709  mptsnun  36711  dissneqlem  36712  dissneq  36713  fvineqsnf1  36782  lindsadd  36975  lindsenlbs  36977  poimirlem4  36986  poimirlem25  37007  poimirlem26  37008  poimirlem27  37009  poimirlem31  37013  poimirlem32  37014  heiborlem3  37175  ismrer1  37200  lshpnel2N  38349  lsatlspsn2  38356  lsatlspsn  38357  lsatspn0  38364  lkrscss  38462  lfl1dim  38485  lfl1dim2N  38486  ldualvs  38501  atpointN  39108  watvalN  39358  trnsetN  39521  dih1dimatlem  40694  dihatexv  40703  dihjat1lem  40793  dihjat1  40794  lcfl7N  40866  lcfl8  40867  lcfl9a  40870  lcfrlem8  40914  lcfrlem9  40915  lcf1o  40916  mapdval2N  40995  mapdval4N  40997  mapdspex  41033  mapdn0  41034  mapdpglem23  41059  mapdpg  41071  mapdindp1  41085  mapdheq  41093  hvmapval  41125  mapdh9a  41154  hdmap1eq  41166  hdmap1cbv  41167  hdmapval  41193  hdmap10  41205  hdmaplkr  41278  sn-iotalem  41535  evlsvvval  41628  evlsevl  41636  0prjspnrel  41883  mzpclval  41977  mzpcl1  41981  wopprc  42283  dnnumch3lem  42302  aomclem8  42317  mendvsca  42447  cytpval  42465  snen1g  42789  k0004lem3  43414  dvconstbi  43607  wessf1ornlem  44394  dvmptfprodlem  45170  fourierdlem32  45365  fourierdlem33  45366  fourierdlem48  45380  funressnmo  46266  aiotajust  46302  funressndmafv2rn  46441  fzopredsuc  46541  elsprel  46653  opeliun2xp  47222  dmmpossx2  47226  lindslinindsimp2  47357  ldepspr  47367  ldepsnlinc  47402  line  47631  rrxline  47633  setc2othin  47888  mndtcval  47917  mndtcbas  47919