Theorem sneq 4590

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

Syntax hints:   → wi 4   = wceq 1541  {cab 2714  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-sn 4581

This theorem is referenced by:  sneqi  4591  sneqd  4592  euabsn  4683  absneu  4685  preq1  4690  tpeq3  4701  issn  4788  mosneq  4798  sneqbg  4799  opeq1  4829  snexg  5380  propeqop  5455  opthwiener  5462  otiunsndisj  5468  opeliunxp  5691  opeliun2xp  5692  relop  5799  inisegn0  6057  xpdifid  6126  dmsnsnsn  6178  predeq123  6260  iotajust  6447  iotanul2  6465  fconstg  6721  f1osng  6816  opabiotafun  6914  fvn0ssdmfun  7019  fsng  7082  fsn2g  7083  fnressn  7103  fressnfv  7105  funfvima3  7182  f12dfv  7219  f13dfv  7220  isofrlem  7286  isoselem  7287  elxp4  7864  elxp5  7865  1stval  7935  2ndval  7936  2ndval2  7951  fo1st  7953  fo2nd  7954  f1stres  7957  f2ndres  7958  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8035  fparlem3  8056  fparlem4  8057  xpord2pred  8087  xpord3pred  8094  suppval  8104  suppsnop  8120  ressuppssdif  8127  brtpos2  8174  dftpos4  8187  tpostpos  8188  naddcllem  8604  eceq1  8674  fvdiagfn  8829  mapsncnv  8831  elixpsn  8875  ixpsnf1o  8876  ensn1g  8959  en1  8961  difsnen  8987  xpsneng  8990  xpcomco  8995  xpassen  8999  xpdom2  9000  canth2  9058  rexdif1en  9085  cnvfi  9100  marypha2lem2  9339  cardsn  9881  pm54.43  9913  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem9  10069  kmlem11  10071  kmlem12  10072  ackbij1lem8  10136  r1om  10153  fictb  10154  hsmexlem4  10339  axcc2lem  10346  axcc2  10347  axdc3lem4  10363  fpwwe2cbv  10541  fpwwe2lem3  10544  fpwwecbv  10555  canth4  10558  s3iunsndisj  14891  fsum2dlem  15693  fsumcnv  15696  fsumcom2  15697  ackbijnn  15751  fprod2dlem  15903  fprodcnv  15906  fprodcom2  15907  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfunsn  16571  vdwlem1  16909  vdwlem12  16920  vdwlem13  16921  vdwnn  16926  0ram  16948  ramz2  16952  pwsval  17406  symg2bas  19322  symgfixelsi  19364  pmtrfv  19381  pmtrprfval  19416  sylow2a  19548  efgrelexlema  19678  gsum2dlem2  19900  gsum2d2  19903  gsumcom2  19904  dprdcntz  19939  dprddisj  19940  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  ablfac1eu  20004  ablfaclem3  20018  lssats2  20951  lspsneq0  20963  lbsind  21032  lspsneq  21077  lspdisj2  21082  lspsnsubn0  21095  lspprat  21108  islbs2  21109  lbsextlem4  21116  lbsextg  21117  lpi0  21281  lpi1  21282  irinitoringc  21434  pzriprnglem13  21448  pzriprnglem14  21449  frlmlbs  21752  lindfind  21771  lindsind  21772  lindfrn  21776  psrvsca  21905  evlsvvval  22048  evlssca  22049  mpfind  22070  coe1fv  22147  coe1tm  22215  pf1ind  22299  submaval  22525  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  islp  23084  perfi  23099  t1sncld  23270  bwth  23354  dis2ndc  23404  nllyi  23419  dissnlocfin  23473  ptbasfi  23525  txkgen  23596  xkofvcn  23628  xkoinjcn  23631  qtopeu  23660  txswaphmeolem  23748  pt1hmeo  23750  elflim2  23908  cnextfvval  24009  cnextcn  24011  cnextfres1  24012  cnextfres  24013  tsmsxplem1  24097  tsmsxplem2  24098  ucncn  24228  itg11  25648  i1faddlem  25650  i1fmullem  25651  itg1addlem3  25655  itg1mulc  25661  eldv  25855  ply1lpir  26143  areambl  26924  conway  27775  cutsval  27776  cutcuts  27777  cutbday  27780  eqcuts  27781  eqcuts2  27782  cutsun12  27786  cutbdaybnd  27791  cutbdaybnd2  27792  cutbdaylt  27794  eqcuts3  27800  bday1  27810  cuteq0  27811  cuteq1  27813  madebdaylemlrcut  27895  sltsbday  27913  cofcut1  27916  cofcutr  27920  oniso  28267  bdayn0p1  28365  expsval  28421  pw2cut2  28458  tglngval  28623  edglnl  29216  nbgrval  29409  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  nbgr1vtx  29431  nb3grprlem2  29454  uvtxel  29461  uvtxel1  29469  uvtxusgrel  29476  cusgredg  29497  cplgr1v  29503  cplgr3v  29508  usgredgsscusgredg  29533  vtxdgval  29542  1loopgrvd2  29577  wlk1walk  29712  wlkres  29742  wlkp1lem8  29752  usgr2pthlem  29836  crctcshwlkn0lem6  29888  2wspiundisj  30039  clwwlknon1  30172  1wlkdlem4  30215  eupth2lem3lem3  30305  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3v  30350  1vwmgr  30351  3vfriswmgr  30353  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrwopreglem4a  30385  h1de2ctlem  31630  spansn  31634  elspansn  31641  elspansn2  31642  spansneleq  31645  h1datom  31657  spansnj  31722  spansncv  31728  superpos  32429  sumdmdlem2  32494  aciunf1lem  32740  fnpreimac  32749  dfcnv2  32754  pwrssmgc  33082  gsummpt2co  33131  gsumpart  33146  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  0nellinds  33451  lindssn  33459  lsmsnidl  33480  nsgmgclem  33492  nsgmgc  33493  nsgqusf1olem1  33494  nsgqusf1olem2  33495  nsgqusf1olem3  33496  pidlnzb  33503  elrspunidl  33509  extvfval  33697  lbslsat  33773  lindsunlem  33781  extdgval  33810  fldextrspunlsplem  33830  locfinreflem  33997  esum2dlem  34249  sibfima  34495  sibfof  34497  bnj1373  35186  bnj1489  35212  funen1cnv  35244  fineqvac  35272  cplgredgex  35315  pfxwlk  35318  revwlk  35319  loop1cycl  35331  cvmscbv  35452  cvmsdisj  35464  cvmsss2  35468  cvmliftlem15  35492  cvmlift2lem11  35507  cvmlift2lem12  35508  cvmlift2lem13  35509  satffunlem1lem1  35596  satffunlem2lem1  35598  mvtinf  35749  eldm3  35955  elima4  35970  fvsingle  36112  snelsingles  36114  dfiota3  36115  brapply  36130  funpartlem  36136  altopeq12  36156  ranksng  36361  neibastop3  36556  tailval  36567  filnetlem4  36575  bj-snexg  37235  bj-restsnss  37288  bj-restsnss2  37289  f1omptsnlem  37541  f1omptsn  37542  mptsnun  37544  dissneqlem  37545  dissneq  37546  fvineqsnf1  37615  lindsadd  37814  lindsenlbs  37816  poimirlem4  37825  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  poimirlem32  37853  heiborlem3  38014  ismrer1  38039  lshpnel2N  39245  lsatlspsn2  39252  lsatlspsn  39253  lsatspn0  39260  lkrscss  39358  lfl1dim  39381  lfl1dim2N  39382  ldualvs  39397  atpointN  40003  watvalN  40253  trnsetN  40416  dih1dimatlem  41589  dihatexv  41598  dihjat1lem  41688  dihjat1  41689  lcfl7N  41761  lcfl8  41762  lcfl9a  41765  lcfrlem8  41809  lcfrlem9  41810  lcf1o  41811  mapdval2N  41890  mapdval4N  41892  mapdspex  41928  mapdn0  41929  mapdpglem23  41954  mapdpg  41966  mapdindp1  41980  mapdheq  41988  hvmapval  42020  mapdh9a  42049  hdmap1eq  42061  hdmap1cbv  42062  hdmapval  42088  hdmap10  42100  hdmaplkr  42173  sn-iotalem  42477  evlsevl  42817  0prjspnrel  42870  mzpclval  42967  mzpcl1  42971  wopprc  43272  dnnumch3lem  43288  aomclem8  43303  mendvsca  43429  cytpval  43444  snen1g  43765  k0004lem3  44390  dvconstbi  44575  relpfrlem  45194  permaxinf2lem  45253  wessf1ornlem  45429  dvmptfprodlem  46188  fourierdlem32  46383  fourierdlem33  46384  fourierdlem48  46398  funressnmo  47292  aiotajust  47330  funressndmafv2rn  47469  fzopredsuc  47569  elsprel  47721  clnbgrval  48068  dfvopnbgr2  48099  vopnbgrel  48100  dfclnbgr6  48102  dfnbgr6  48103  cycl3grtri  48193  dmmpossx2  48583  lindslinindsimp2  48709  ldepspr  48719  ldepsnlinc  48754  line  48978  rrxline  48980  dftpos5  49119  tposideq  49133  initc  49336  setc2othin  49711  functermceu  49755  idfudiag1  49770  funcsn  49786  0fucterm  49788  mndtcval  49824  mndtcbas  49826