Theorem sneq 4637

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 2745	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2802	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4628	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4628	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cab 2710  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-sn 4628

This theorem is referenced by:  sneqi  4638  sneqd  4639  euabsn  4729  absneu  4731  preq1  4736  tpeq3  4747  issn  4832  mosneq  4842  sneqbg  4843  opeq1  4872  snexg  5429  propeqop  5506  opthwiener  5513  otiunsndisj  5519  opeliunxp  5741  relop  5848  elimasngOLD  6086  inisegn0  6094  xpdifid  6164  dmsnsnsn  6216  predeq123  6298  suceq  6427  iotajust  6491  iotanul2  6510  fconstg  6775  f1osng  6871  opabiotafun  6968  fvn0ssdmfun  7072  fsng  7130  fsn2g  7131  fnressn  7151  fressnfv  7153  funfvima3  7233  f12dfv  7266  f13dfv  7267  isofrlem  7332  isoselem  7333  elxp4  7908  elxp5  7909  1stval  7972  2ndval  7973  2ndval2  7988  fo1st  7990  fo2nd  7991  f1stres  7994  f2ndres  7995  mpomptsx  8045  dmmpossx  8047  fmpox  8048  ovmptss  8074  fparlem3  8095  fparlem4  8096  xpord2pred  8126  xpord3pred  8133  suppval  8143  suppsnop  8158  ressuppssdif  8165  brtpos2  8212  dftpos4  8225  tpostpos  8226  naddcllem  8671  eceq1  8737  fvdiagfn  8881  mapsncnv  8883  elixpsn  8927  ixpsnf1o  8928  ensn1g  9015  en1  9017  en1OLD  9018  difsnen  9049  xpsneng  9052  xpcomco  9058  xpassen  9062  xpdom2  9063  canth2  9126  rexdif1en  9154  rexdif1enOLD  9155  cnvfi  9176  phplem3OLD  9215  xpfiOLD  9314  marypha2lem2  9427  cardsn  9960  pm54.43  9992  dfac5lem3  10116  dfac5lem4  10117  kmlem9  10149  kmlem11  10151  kmlem12  10152  ackbij1lem8  10218  r1om  10235  fictb  10236  hsmexlem4  10420  axcc2lem  10427  axcc2  10428  axdc3lem4  10444  fpwwe2cbv  10621  fpwwe2lem3  10624  fpwwecbv  10635  canth4  10638  s3iunsndisj  14911  fsum2dlem  15712  fsumcnv  15715  fsumcom2  15716  ackbijnn  15770  fprod2dlem  15920  fprodcnv  15923  fprodcom2  15924  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  lcmfunsnlem2  16573  lcmfunsn  16577  vdwlem1  16910  vdwlem12  16921  vdwlem13  16922  vdwnn  16927  0ram  16949  ramz2  16953  pwsval  17428  symg2bas  19253  symgfixelsi  19296  pmtrfv  19313  pmtrprfval  19348  sylow2a  19480  efgrelexlema  19610  gsum2dlem2  19831  gsum2d2  19834  gsumcom2  19835  dprdcntz  19870  dprddisj  19871  dprd2dlem2  19902  dprd2dlem1  19903  dprd2da  19904  ablfac1eu  19935  ablfaclem3  19949  lssats2  20599  lspsneq0  20611  lbsind  20679  lspsneq  20723  lspdisj2  20728  lspsnsubn0  20741  lspprat  20754  islbs2  20755  lbsextlem4  20762  lbsextg  20763  lpi0  20872  lpi1  20873  frlmlbs  21336  lindfind  21355  lindsind  21356  lindfrn  21360  psrvsca  21492  evlssca  21634  mpfind  21652  coe1fv  21712  coe1tm  21777  pf1ind  21856  submaval  22065  mdetunilem3  22098  mdetunilem4  22099  mdetunilem9  22104  islp  22626  perfi  22641  t1sncld  22812  bwth  22896  dis2ndc  22946  nllyi  22961  dissnlocfin  23015  ptbasfi  23067  txkgen  23138  xkofvcn  23170  xkoinjcn  23173  qtopeu  23202  txswaphmeolem  23290  pt1hmeo  23292  elflim2  23450  cnextfvval  23551  cnextcn  23553  cnextfres1  23554  cnextfres  23555  tsmsxplem1  23639  tsmsxplem2  23640  ucncn  23772  itg11  25190  i1faddlem  25192  i1fmullem  25193  itg1addlem3  25197  itg1mulc  25204  eldv  25397  ply1lpir  25678  areambl  26443  conway  27280  scutval  27281  scutcut  27282  scutbday  27285  eqscut  27286  eqscut2  27287  scutun12  27291  scutbdaybnd  27296  scutbdaybnd2  27297  scutbdaylt  27299  bday1s  27312  cuteq0  27313  cuteq1  27314  madebdaylemlrcut  27373  cofcut1  27387  cofcutr  27391  tglngval  27782  edglnl  28383  nbgrval  28573  nbgr2vtx1edg  28587  nbuhgr2vtx1edgb  28589  nbgr1vtx  28595  nb3grprlem2  28618  uvtxel  28625  uvtxel1  28633  uvtxusgrel  28640  cusgredg  28661  cplgr1v  28667  cplgr3v  28672  usgredgsscusgredg  28696  vtxdgval  28705  1loopgrvd2  28740  wlk1walk  28876  wlkres  28907  wlkp1lem8  28917  usgr2pthlem  29000  crctcshwlkn0lem6  29049  2wspiundisj  29197  clwwlknon1  29330  1wlkdlem4  29373  eupth2lem3lem3  29463  frcond1  29499  frgr1v  29504  nfrgr2v  29505  frgr3v  29508  1vwmgr  29509  3vfriswmgr  29511  3cyclfrgrrn1  29518  n4cyclfrgr  29524  frgrwopreglem4a  29543  h1de2ctlem  30786  spansn  30790  elspansn  30797  elspansn2  30798  spansneleq  30801  h1datom  30813  spansnj  30878  spansncv  30884  superpos  31585  sumdmdlem2  31650  aciunf1lem  31865  fnpreimac  31874  dfcnv2  31879  pwrssmgc  32148  gsummpt2co  32178  gsumpart  32185  0nellinds  32452  lindssn  32459  lsmsnidl  32474  nsgmgclem  32485  nsgmgc  32486  nsgqusf1olem1  32487  nsgqusf1olem2  32488  nsgqusf1olem3  32489  elrspunidl  32504  lbslsat  32646  lindsunlem  32654  extdgval  32678  locfinreflem  32758  esum2dlem  33028  sibfima  33275  sibfof  33277  bnj1373  33979  bnj1489  34005  funen1cnv  34029  fineqvac  34035  cplgredgex  34049  pfxwlk  34052  revwlk  34053  loop1cycl  34066  cvmscbv  34187  cvmsdisj  34199  cvmsss2  34203  cvmliftlem15  34227  cvmlift2lem11  34242  cvmlift2lem12  34243  cvmlift2lem13  34244  satffunlem1lem1  34331  satffunlem2lem1  34333  mvtinf  34484  eldm3  34669  elima4  34685  fvsingle  34830  snelsingles  34832  dfiota3  34833  brapply  34848  funpartlem  34852  altopeq12  34872  ranksng  35077  neibastop3  35185  tailval  35196  filnetlem4  35204  bj-snexg  35853  bj-restsnss  35902  bj-restsnss2  35903  f1omptsnlem  36155  f1omptsn  36156  mptsnun  36158  dissneqlem  36159  dissneq  36160  fvineqsnf1  36229  lindsadd  36419  lindsenlbs  36421  poimirlem4  36430  poimirlem25  36451  poimirlem26  36452  poimirlem27  36453  poimirlem31  36457  poimirlem32  36458  heiborlem3  36619  ismrer1  36644  lshpnel2N  37793  lsatlspsn2  37800  lsatlspsn  37801  lsatspn0  37808  lkrscss  37906  lfl1dim  37929  lfl1dim2N  37930  ldualvs  37945  atpointN  38552  watvalN  38802  trnsetN  38965  dih1dimatlem  40138  dihatexv  40147  dihjat1lem  40237  dihjat1  40238  lcfl7N  40310  lcfl8  40311  lcfl9a  40314  lcfrlem8  40358  lcfrlem9  40359  lcf1o  40360  mapdval2N  40439  mapdval4N  40441  mapdspex  40477  mapdn0  40478  mapdpglem23  40503  mapdpg  40515  mapdindp1  40529  mapdheq  40537  hvmapval  40569  mapdh9a  40598  hdmap1eq  40610  hdmap1cbv  40611  hdmapval  40637  hdmap10  40649  hdmaplkr  40722  sn-iotalem  40986  evlsvvval  41085  evlsevl  41093  0prjspnrel  41313  mzpclval  41396  mzpcl1  41400  wopprc  41702  dnnumch3lem  41721  aomclem8  41736  mendvsca  41866  cytpval  41884  snen1g  42208  k0004lem3  42833  dvconstbi  43026  wessf1ornlem  43815  dvmptfprodlem  44595  fourierdlem32  44790  fourierdlem33  44791  fourierdlem48  44805  funressnmo  45691  aiotajust  45727  funressndmafv2rn  45866  fzopredsuc  45966  elsprel  46078  irinitoringc  46869  opeliun2xp  46910  dmmpossx2  46914  lindslinindsimp2  47046  ldepspr  47056  ldepsnlinc  47091  line  47320  rrxline  47322  setc2othin  47578  mndtcval  47607  mndtcbas  47609