Theorem sneq 4658

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 2752	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2811	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4649	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4649	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1537  {cab 2717  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-sn 4649

This theorem is referenced by:  sneqi  4659  sneqd  4660  euabsn  4751  absneu  4753  preq1  4758  tpeq3  4769  issn  4857  mosneq  4867  sneqbg  4868  opeq1  4897  snexg  5450  propeqop  5526  opthwiener  5533  otiunsndisj  5539  opeliunxp  5767  relop  5875  elimasngOLD  6120  inisegn0  6128  xpdifid  6199  dmsnsnsn  6251  predeq123  6333  suceq  6461  iotajust  6524  iotanul2  6543  fconstg  6808  f1osng  6903  opabiotafun  7002  fvn0ssdmfun  7108  fsng  7171  fsn2g  7172  fnressn  7192  fressnfv  7194  funfvima3  7273  f12dfv  7309  f13dfv  7310  isofrlem  7376  isoselem  7377  elxp4  7962  elxp5  7963  1stval  8032  2ndval  8033  2ndval2  8048  fo1st  8050  fo2nd  8051  f1stres  8054  f2ndres  8055  mpomptsx  8105  dmmpossx  8107  fmpox  8108  ovmptss  8134  fparlem3  8155  fparlem4  8156  xpord2pred  8186  xpord3pred  8193  suppval  8203  suppsnop  8219  ressuppssdif  8226  brtpos2  8273  dftpos4  8286  tpostpos  8287  naddcllem  8732  eceq1  8802  fvdiagfn  8949  mapsncnv  8951  elixpsn  8995  ixpsnf1o  8996  ensn1g  9084  en1  9086  en1OLD  9087  difsnen  9119  xpsneng  9122  xpcomco  9128  xpassen  9132  xpdom2  9133  canth2  9196  rexdif1en  9224  rexdif1enOLD  9225  cnvfi  9243  phplem3OLD  9282  xpfiOLD  9387  marypha2lem2  9505  cardsn  10038  pm54.43  10070  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem9  10228  kmlem11  10230  kmlem12  10231  ackbij1lem8  10295  r1om  10312  fictb  10313  hsmexlem4  10498  axcc2lem  10505  axcc2  10506  axdc3lem4  10522  fpwwe2cbv  10699  fpwwe2lem3  10702  fpwwecbv  10713  canth4  10716  s3iunsndisj  15017  fsum2dlem  15818  fsumcnv  15821  fsumcom2  15822  ackbijnn  15876  fprod2dlem  16028  fprodcnv  16031  fprodcom2  16032  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  lcmfunsn  16691  vdwlem1  17028  vdwlem12  17039  vdwlem13  17040  vdwnn  17045  0ram  17067  ramz2  17071  pwsval  17546  symg2bas  19434  symgfixelsi  19477  pmtrfv  19494  pmtrprfval  19529  sylow2a  19661  efgrelexlema  19791  gsum2dlem2  20013  gsum2d2  20016  gsumcom2  20017  dprdcntz  20052  dprddisj  20053  dprd2dlem2  20084  dprd2dlem1  20085  dprd2da  20086  ablfac1eu  20117  ablfaclem3  20131  lssats2  21021  lspsneq0  21033  lbsind  21102  lspsneq  21147  lspdisj2  21152  lspsnsubn0  21165  lspprat  21178  islbs2  21179  lbsextlem4  21186  lbsextg  21187  lpi0  21359  lpi1  21360  irinitoringc  21513  pzriprnglem13  21527  pzriprnglem14  21528  frlmlbs  21840  lindfind  21859  lindsind  21860  lindfrn  21864  psrvsca  21992  evlssca  22136  mpfind  22154  coe1fv  22229  coe1tm  22297  pf1ind  22380  submaval  22608  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  islp  23169  perfi  23184  t1sncld  23355  bwth  23439  dis2ndc  23489  nllyi  23504  dissnlocfin  23558  ptbasfi  23610  txkgen  23681  xkofvcn  23713  xkoinjcn  23716  qtopeu  23745  txswaphmeolem  23833  pt1hmeo  23835  elflim2  23993  cnextfvval  24094  cnextcn  24096  cnextfres1  24097  cnextfres  24098  tsmsxplem1  24182  tsmsxplem2  24183  ucncn  24315  itg11  25745  i1faddlem  25747  i1fmullem  25748  itg1addlem3  25752  itg1mulc  25759  eldv  25953  ply1lpir  26241  areambl  27019  conway  27862  scutval  27863  scutcut  27864  scutbday  27867  eqscut  27868  eqscut2  27869  scutun12  27873  scutbdaybnd  27878  scutbdaybnd2  27879  scutbdaylt  27881  bday1s  27894  cuteq0  27895  cuteq1  27896  madebdaylemlrcut  27955  cofcut1  27972  cofcutr  27976  expsval  28426  tglngval  28577  edglnl  29178  nbgrval  29371  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nbgr1vtx  29393  nb3grprlem2  29416  uvtxel  29423  uvtxel1  29431  uvtxusgrel  29438  cusgredg  29459  cplgr1v  29465  cplgr3v  29470  usgredgsscusgredg  29495  vtxdgval  29504  1loopgrvd2  29539  wlk1walk  29675  wlkres  29706  wlkp1lem8  29716  usgr2pthlem  29799  crctcshwlkn0lem6  29848  2wspiundisj  29996  clwwlknon1  30129  1wlkdlem4  30172  eupth2lem3lem3  30262  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  1vwmgr  30308  3vfriswmgr  30310  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrwopreglem4a  30342  h1de2ctlem  31587  spansn  31591  elspansn  31598  elspansn2  31599  spansneleq  31602  h1datom  31614  spansnj  31679  spansncv  31685  superpos  32386  sumdmdlem2  32451  aciunf1lem  32680  fnpreimac  32689  dfcnv2  32694  pwrssmgc  32973  gsummpt2co  33031  gsumpart  33038  0nellinds  33363  lindssn  33371  lsmsnidl  33392  nsgmgclem  33404  nsgmgc  33405  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  pidlnzb  33415  elrspunidl  33421  lbslsat  33629  lindsunlem  33637  extdgval  33667  locfinreflem  33786  esum2dlem  34056  sibfima  34303  sibfof  34305  bnj1373  35006  bnj1489  35032  funen1cnv  35064  fineqvac  35073  cplgredgex  35088  pfxwlk  35091  revwlk  35092  loop1cycl  35105  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  cvmliftlem15  35266  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift2lem13  35283  satffunlem1lem1  35370  satffunlem2lem1  35372  mvtinf  35523  eldm3  35723  elima4  35739  fvsingle  35884  snelsingles  35886  dfiota3  35887  brapply  35902  funpartlem  35906  altopeq12  35926  ranksng  36131  neibastop3  36328  tailval  36339  filnetlem4  36347  bj-snexg  37000  bj-restsnss  37049  bj-restsnss2  37050  f1omptsnlem  37302  f1omptsn  37303  mptsnun  37305  dissneqlem  37306  dissneq  37307  fvineqsnf1  37376  lindsadd  37573  lindsenlbs  37575  poimirlem4  37584  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  heiborlem3  37773  ismrer1  37798  lshpnel2N  38941  lsatlspsn2  38948  lsatlspsn  38949  lsatspn0  38956  lkrscss  39054  lfl1dim  39077  lfl1dim2N  39078  ldualvs  39093  atpointN  39700  watvalN  39950  trnsetN  40113  dih1dimatlem  41286  dihatexv  41295  dihjat1lem  41385  dihjat1  41386  lcfl7N  41458  lcfl8  41459  lcfl9a  41462  lcfrlem8  41506  lcfrlem9  41507  lcf1o  41508  mapdval2N  41587  mapdval4N  41589  mapdspex  41625  mapdn0  41626  mapdpglem23  41651  mapdpg  41663  mapdindp1  41677  mapdheq  41685  hvmapval  41717  mapdh9a  41746  hdmap1eq  41758  hdmap1cbv  41759  hdmapval  41785  hdmap10  41797  hdmaplkr  41870  sn-iotalem  42214  evlsvvval  42518  evlsevl  42526  0prjspnrel  42582  mzpclval  42681  mzpcl1  42685  wopprc  42987  dnnumch3lem  43003  aomclem8  43018  mendvsca  43148  cytpval  43163  snen1g  43486  k0004lem3  44111  dvconstbi  44303  wessf1ornlem  45092  dvmptfprodlem  45865  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  funressnmo  46961  aiotajust  46999  funressndmafv2rn  47138  fzopredsuc  47238  elsprel  47349  clnbgrval  47696  dfvopnbgr2  47725  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  opeliun2xp  48057  dmmpossx2  48061  lindslinindsimp2  48192  ldepspr  48202  ldepsnlinc  48237  line  48466  rrxline  48468  setc2othin  48723  mndtcval  48752  mndtcbas  48754