Theorem snex 5192

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5140. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsn2 4457	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4550	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 559	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2852	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5191	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3488	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	syl5eqel 2872	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4532	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 208	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5072	. . 3 ⊢ ∅ ∈ V
11	9, 10	syl6eqel 2876	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 177	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1508   ∈ wcel 2051  Vcvv 3417  ∅c0 4181  {csn 4444  {cpr 4446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752  ax-sep 5064  ax-nul 5071  ax-pr 5190

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-dif 3834  df-un 3836  df-nul 4182  df-sn 4445  df-pr 4447

This theorem is referenced by:  prex  5193  sels  5194  elALT  5195  dtruALT2  5196  snelpwi  5197  snelpw  5198  rext  5201  sspwb  5202  intid  5211  moabex  5212  nnullss  5215  exss  5216  elopg  5219  opi1  5221  op1stb  5224  opnz  5226  opeqsng  5253  opeqpr  5255  snopeqop  5256  opthwiener  5264  uniop  5265  0sn0ep  5326  frirr  5388  opthprc  5470  frsn  5493  xpsspw  5536  relop  5575  snsn0non  6152  onnev  6154  funopg  6227  funsneqopb  6743  fsnex  6870  tpex  7293  snnex  7303  difsnexi  7306  sucexb  7346  soex  7447  elxp4  7448  elxp5  7449  fvclex  7478  opabex3d  7484  opabex3rd  7485  opabex3  7486  1stval  7509  2ndval  7510  fo1st  7527  fo2nd  7528  mpoexxg  7587  cnvf1o  7620  fnse  7638  suppsnop  7653  brtpos2  7707  wfrlem15  7779  tfrlem12  7835  tfrlem16  7839  mapsnd  8254  fvdiagfn  8259  mapsnconst  8260  mapsncnv  8261  mapsnf1o2  8262  ralxpmap  8264  elixpsn  8304  ixpsnf1o  8305  mapsnf1o  8306  ensn1  8376  en1b  8380  2dom  8385  mapsnend  8391  snmapen  8393  xpsnen  8403  endisj  8406  xpsnen2g  8412  domunsncan  8419  enfixsn  8428  domunsn  8469  fodomr  8470  disjenex  8477  domssex2  8479  domssex  8480  map2xp  8489  phplem2  8499  isinf  8532  pssnn  8537  findcard2  8559  ac6sfi  8563  xpfi  8590  fodomfi  8598  pwfilem  8619  fczfsuppd  8652  snopfsupp  8657  fisn  8692  marypha1lem  8698  brwdom2  8838  unxpwdom2  8853  elirrv  8861  epfrs  8973  tc2  8984  tcsni  8985  ranksuc  9094  djuex  9137  fseqenlem1  9250  dfac5lem2  9350  dfac5lem3  9351  dfac5lem4  9352  kmlem2  9377  cdaval  9395  djuassen  9408  mapdjuen  9410  djudom1  9412  djuinf  9418  ackbij1lem5  9450  cfsuc  9483  isfin1-3  9612  hsmexlem4  9655  axcc2lem  9662  dcomex  9673  axdc3lem4  9679  axdc4lem  9681  ttukeylem3  9737  brdom7disj  9757  brdom6disj  9758  fpwwe2lem13  9868  canthwe  9877  canthp1lem1  9878  uniwun  9966  rankcf  10003  nn0ex  11720  hashxplem  13613  hashmap  13615  hashbclem  13629  hashf1lem1  13632  hashge3el3dif  13661  ofs1  14197  climconst2  14772  incexclem  15057  ramub1lem2  16225  cshwsex  16296  setsvalg  16374  setsid  16400  pwsbas  16622  pwsle  16627  pwssca  16631  pwssnf1o  16633  imasplusg  16652  imasmulr  16653  imasvsca  16655  imasip  16656  xpsc  16692  acsfn  16800  isfunc  17004  homaf  17160  homaval  17161  funcsetcestrclem1  17274  mgm1  17737  sgrp1  17773  mnd1  17811  mnd1id  17812  grp1  18005  grp1inv  18006  mulgfval  18025  symg2bas  18299  idrespermg  18312  pmtrsn  18421  psgnsn  18422  abl1  18754  gsum2d2  18859  gsumcom2  18860  dprdz  18914  dprdsn  18920  dprd2da  18926  ring1  19087  pwssplit3  19567  rng1nnzr  19780  evlssca  20027  mpfind  20041  evls1sca  20204  pf1ind  20235  frlmip  20639  islindf4  20699  mattposvs  20783  mat1dimelbas  20799  mat1dimscm  20803  mat1dimmul  20804  mat1rhmval  20807  m1detdiag  20925  mdetrlin  20930  mdetrsca2  20932  mdetrlin2  20935  mdetunilem5  20944  smadiadetglem2  21000  basdif0  21280  ordtbas  21519  leordtval2  21539  dishaus  21709  discmp  21725  conncompid  21758  dis2ndc  21787  dislly  21824  dis1stc  21826  unisngl  21854  1stckgen  21881  ptbasfi  21908  dfac14lem  21944  dfac14  21945  ptrescn  21966  xkoptsub  21981  pt1hmeo  22133  xpstopnlem1  22136  ptcmpfi  22140  isufil2  22235  ufileu  22246  filufint  22247  uffix  22248  uffixsn  22252  flimclslem  22311  ptcmplem1  22379  cnextfval  22389  imasdsf1olem  22701  icccmplem1  23148  icccmplem2  23149  rrxip  23711  rrxsca  23717  ehl1eudis  23741  elply2  24504  plyss  24507  plyeq0lem  24518  taylfval  24665  axlowdimlem15  26460  axlowdim  26465  snstriedgval  26541  vtxvalsnop  26544  iedgvalsnop  26545  upgr1eop  26618  upgr1eopALT  26620  uspgr1eop  26747  usgr1eop  26750  lfuhgr1v0e  26754  1loopgrvd2  27003  1loopgrvd0  27004  p1evtxdeqlem  27012  p1evtxdeq  27013  p1evtxdp1  27014  uspgrloopvtx  27015  uspgrloopiedg  27017  uspgrloopedg  27018  wlkp1lem4  27179  0pthonv  27673  eupth2lem3  27781  wlkl0  27935  0ofval  28356  suppovss  30204  resf1o  30242  ordtconnlem1  30843  esumpr  31001  esumrnmpt2  31003  esumfzf  31004  esum2dlem  31027  esum2d  31028  esumiun  31029  prsiga  31067  rossros  31116  cntnevol  31164  carsgclctunlem1  31252  omsmeas  31258  eulerpartlemgs2  31315  ccatmulgnn0dir  31490  ofcs1  31492  actfunsnf1o  31555  actfunsnrndisj  31556  reprsuc  31566  breprexplema  31581  bnj918  31717  bnj95  31815  bnj1452  32001  bnj1489  32005  subfacp1lem5  32056  erdszelem5  32067  erdszelem8  32070  cvmliftlem4  32160  cvmliftlem5  32161  cvmlift2lem6  32180  cvmlift2lem9  32183  cvmlift2lem12  32186  frrlem13  32696  conway  32825  etasslt  32835  slerec  32838  fobigcup  32922  elsingles  32940  fnsingle  32941  fvsingle  32942  dfiota3  32945  brapply  32960  brsuccf  32963  funpartlem  32964  altopthsn  32983  altxpsspw  32999  hfsn  33201  neibastop2lem  33269  topjoin  33274  onpsstopbas  33338  bj-snsetex  33833  bj-elsngl  33838  bj-2uplex  33892  bj-restsn  33923  bj-snmoore  33956  f1omptsnlem  34099  mptsnunlem  34101  topdifinffinlem  34110  finixpnum  34358  ptrest  34372  poimirlem3  34376  poimirlem4  34377  poimirlem28  34401  fdc  34502  heiborlem3  34573  heiborlem8  34578  ismrer1  34598  grposnOLD  34642  zrdivrng  34713  ecexALTV  35073  eccnvepex  35077  ldualset  35746  lineset  36359  ispointN  36363  dvaset  37626  dvhset  37702  dibval  37763  dibfna  37775  frlmsnic  38627  elrfi  38727  mzpincl  38767  mzpcompact2lem  38784  wopprc  39064  dfac11  39099  kelac2  39102  pwslnmlem1  39129  pwslnm  39131  fvilbdRP  39439  brtrclfv2  39476  frege110  39723  frege133  39746  k0004lem3  39903  mnuprdlem1  40024  mnuprdlem2  40025  triv1nsgd  40057  1nsgtrivd  40058  simpgnsgd  40075  2nsgsimpgd  40077  snelpwrVD  40624  fnchoice  40745  mpct  40925  elmapsnd  40928  difmapsn  40936  unirnmapsn  40938  ssmapsn  40940  limcresiooub  41389  limcresioolb  41390  cnfdmsn  41630  dvsinax  41662  fourierdlem48  41905  fourierdlem49  41906  salexct3  42091  salgencntex  42092  salgensscntex  42093  sge0sn  42127  sge0p1  42162  sge0xp  42177  ovnovollem1  42404  ovnovollem2  42405  vonvolmbllem  42408  setsv  42979  nnsum3primesprm  43358  mpoexxg2  43785  mapsnop  43792  lindsrng01  43925  snlindsntorlem  43927  snlindsntor  43928  lmod1lem1  43944  lmod1lem2  43945  lmod1lem3  43946  lmod1lem4  43947  lmod1lem5  43948  lmod1  43949  lmod1zr  43950  aacllem  44304