Theorem sneq 4639

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

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

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 4630

This theorem is referenced by:  sneqi  4640  sneqd  4641  euabsn  4731  absneu  4733  preq1  4738  tpeq3  4749  issn  4834  mosneq  4844  sneqbg  4845  opeq1  4874  snexg  5431  propeqop  5508  opthwiener  5515  otiunsndisj  5521  opeliunxp  5744  relop  5851  elimasngOLD  6090  inisegn0  6098  xpdifid  6168  dmsnsnsn  6220  predeq123  6302  suceq  6431  iotajust  6495  iotanul2  6514  fconstg  6779  f1osng  6875  opabiotafun  6973  fvn0ssdmfun  7077  fsng  7135  fsn2g  7136  fnressn  7156  fressnfv  7158  funfvima3  7238  f12dfv  7271  f13dfv  7272  isofrlem  7337  isoselem  7338  elxp4  7913  elxp5  7914  1stval  7977  2ndval  7978  2ndval2  7993  fo1st  7995  fo2nd  7996  f1stres  7999  f2ndres  8000  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  fparlem3  8100  fparlem4  8101  xpord2pred  8131  xpord3pred  8138  suppval  8148  suppsnop  8163  ressuppssdif  8170  brtpos2  8217  dftpos4  8230  tpostpos  8231  naddcllem  8675  eceq1  8741  fvdiagfn  8885  mapsncnv  8887  elixpsn  8931  ixpsnf1o  8932  ensn1g  9019  en1  9021  en1OLD  9022  difsnen  9053  xpsneng  9056  xpcomco  9062  xpassen  9066  xpdom2  9067  canth2  9130  rexdif1en  9158  rexdif1enOLD  9159  cnvfi  9180  phplem3OLD  9219  xpfiOLD  9318  marypha2lem2  9431  cardsn  9964  pm54.43  9996  dfac5lem3  10120  dfac5lem4  10121  kmlem9  10153  kmlem11  10155  kmlem12  10156  ackbij1lem8  10222  r1om  10239  fictb  10240  hsmexlem4  10424  axcc2lem  10431  axcc2  10432  axdc3lem4  10448  fpwwe2cbv  10625  fpwwe2lem3  10628  fpwwecbv  10639  canth4  10642  s3iunsndisj  14915  fsum2dlem  15716  fsumcnv  15719  fsumcom2  15720  ackbijnn  15774  fprod2dlem  15924  fprodcnv  15927  fprodcom2  15928  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfunsn  16581  vdwlem1  16914  vdwlem12  16925  vdwlem13  16926  vdwnn  16931  0ram  16953  ramz2  16957  pwsval  17432  symg2bas  19260  symgfixelsi  19303  pmtrfv  19320  pmtrprfval  19355  sylow2a  19487  efgrelexlema  19617  gsum2dlem2  19839  gsum2d2  19842  gsumcom2  19843  dprdcntz  19878  dprddisj  19879  dprd2dlem2  19910  dprd2dlem1  19911  dprd2da  19912  ablfac1eu  19943  ablfaclem3  19957  lssats2  20611  lspsneq0  20623  lbsind  20691  lspsneq  20735  lspdisj2  20740  lspsnsubn0  20753  lspprat  20766  islbs2  20767  lbsextlem4  20774  lbsextg  20775  lpi0  20885  lpi1  20886  frlmlbs  21352  lindfind  21371  lindsind  21372  lindfrn  21376  psrvsca  21510  evlssca  21652  mpfind  21670  coe1fv  21730  coe1tm  21795  pf1ind  21874  submaval  22083  mdetunilem3  22116  mdetunilem4  22117  mdetunilem9  22122  islp  22644  perfi  22659  t1sncld  22830  bwth  22914  dis2ndc  22964  nllyi  22979  dissnlocfin  23033  ptbasfi  23085  txkgen  23156  xkofvcn  23188  xkoinjcn  23191  qtopeu  23220  txswaphmeolem  23308  pt1hmeo  23310  elflim2  23468  cnextfvval  23569  cnextcn  23571  cnextfres1  23572  cnextfres  23573  tsmsxplem1  23657  tsmsxplem2  23658  ucncn  23790  itg11  25208  i1faddlem  25210  i1fmullem  25211  itg1addlem3  25215  itg1mulc  25222  eldv  25415  ply1lpir  25696  areambl  26463  conway  27300  scutval  27301  scutcut  27302  scutbday  27305  eqscut  27306  eqscut2  27307  scutun12  27311  scutbdaybnd  27316  scutbdaybnd2  27317  scutbdaylt  27319  bday1s  27332  cuteq0  27333  cuteq1  27334  madebdaylemlrcut  27393  cofcut1  27407  cofcutr  27411  tglngval  27802  edglnl  28403  nbgrval  28593  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  nbgr1vtx  28615  nb3grprlem2  28638  uvtxel  28645  uvtxel1  28653  uvtxusgrel  28660  cusgredg  28681  cplgr1v  28687  cplgr3v  28692  usgredgsscusgredg  28716  vtxdgval  28725  1loopgrvd2  28760  wlk1walk  28896  wlkres  28927  wlkp1lem8  28937  usgr2pthlem  29020  crctcshwlkn0lem6  29069  2wspiundisj  29217  clwwlknon1  29350  1wlkdlem4  29393  eupth2lem3lem3  29483  frcond1  29519  frgr1v  29524  nfrgr2v  29525  frgr3v  29528  1vwmgr  29529  3vfriswmgr  29531  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrwopreglem4a  29563  h1de2ctlem  30808  spansn  30812  elspansn  30819  elspansn2  30820  spansneleq  30823  h1datom  30835  spansnj  30900  spansncv  30906  superpos  31607  sumdmdlem2  31672  aciunf1lem  31887  fnpreimac  31896  dfcnv2  31901  pwrssmgc  32170  gsummpt2co  32200  gsumpart  32207  0nellinds  32483  lindssn  32494  lsmsnidl  32509  nsgmgclem  32522  nsgmgc  32523  nsgqusf1olem1  32524  nsgqusf1olem2  32525  nsgqusf1olem3  32526  pidlnzb  32540  elrspunidl  32546  lbslsat  32701  lindsunlem  32709  extdgval  32733  locfinreflem  32820  esum2dlem  33090  sibfima  33337  sibfof  33339  bnj1373  34041  bnj1489  34067  funen1cnv  34091  fineqvac  34097  cplgredgex  34111  pfxwlk  34114  revwlk  34115  loop1cycl  34128  cvmscbv  34249  cvmsdisj  34261  cvmsss2  34265  cvmliftlem15  34289  cvmlift2lem11  34304  cvmlift2lem12  34305  cvmlift2lem13  34306  satffunlem1lem1  34393  satffunlem2lem1  34395  mvtinf  34546  eldm3  34731  elima4  34747  fvsingle  34892  snelsingles  34894  dfiota3  34895  brapply  34910  funpartlem  34914  altopeq12  34934  ranksng  35139  neibastop3  35247  tailval  35258  filnetlem4  35266  bj-snexg  35915  bj-restsnss  35964  bj-restsnss2  35965  f1omptsnlem  36217  f1omptsn  36218  mptsnun  36220  dissneqlem  36221  dissneq  36222  fvineqsnf1  36291  lindsadd  36481  lindsenlbs  36483  poimirlem4  36492  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  heiborlem3  36681  ismrer1  36706  lshpnel2N  37855  lsatlspsn2  37862  lsatlspsn  37863  lsatspn0  37870  lkrscss  37968  lfl1dim  37991  lfl1dim2N  37992  ldualvs  38007  atpointN  38614  watvalN  38864  trnsetN  39027  dih1dimatlem  40200  dihatexv  40209  dihjat1lem  40299  dihjat1  40300  lcfl7N  40372  lcfl8  40373  lcfl9a  40376  lcfrlem8  40420  lcfrlem9  40421  lcf1o  40422  mapdval2N  40501  mapdval4N  40503  mapdspex  40539  mapdn0  40540  mapdpglem23  40565  mapdpg  40577  mapdindp1  40591  mapdheq  40599  hvmapval  40631  mapdh9a  40660  hdmap1eq  40672  hdmap1cbv  40673  hdmapval  40699  hdmap10  40711  hdmaplkr  40784  sn-iotalem  41038  evlsvvval  41135  evlsevl  41143  0prjspnrel  41369  mzpclval  41463  mzpcl1  41467  wopprc  41769  dnnumch3lem  41788  aomclem8  41803  mendvsca  41933  cytpval  41951  snen1g  42275  k0004lem3  42900  dvconstbi  43093  wessf1ornlem  43882  dvmptfprodlem  44660  fourierdlem32  44855  fourierdlem33  44856  fourierdlem48  44870  funressnmo  45756  aiotajust  45792  funressndmafv2rn  45931  fzopredsuc  46031  elsprel  46143  pzriprnglem13  46817  pzriprnglem14  46818  irinitoringc  46967  opeliun2xp  47008  dmmpossx2  47012  lindslinindsimp2  47144  ldepspr  47154  ldepsnlinc  47189  line  47418  rrxline  47420  setc2othin  47676  mndtcval  47705  mndtcbas  47707