Theorem snex 4908

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4852. (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 4190	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4270	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 677	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2686	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 4907	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3266	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	syl5eqel 2705	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4253	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 206	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 4790	. . 3 ⊢ ∅ ∈ V
11	9, 10	syl6eqel 2709	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 176	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1483   ∈ wcel 1990  Vcvv 3200  ∅c0 3915  {csn 4177  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180

This theorem is referenced by:  prex  4909  elALT  4910  dtruALT2  4911  snelpwi  4912  snelpw  4913  rext  4916  sspwb  4917  intid  4926  moabex  4927  nnullss  4930  exss  4931  elopg  4934  opi1  4937  op1stb  4940  opnz  4942  opeqsn  4967  opeqpr  4968  propssopi  4971  opthwiener  4976  uniop  4977  frirr  5091  frsn  5189  xpsspw  5233  relop  5272  onnev  5848  funopg  5922  funsneqopsn  6417  funsneqop  6418  fsnex  6538  tpex  6957  snnex  6966  snnexOLD  6967  difsnexi  6970  sucexb  7009  soex  7109  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  1stval  7170  2ndval  7171  fo1st  7188  fo2nd  7189  mpt2exxg  7244  cnvf1o  7276  fnse  7294  suppsnop  7309  brtpos2  7358  wfrlem15  7429  tfrlem12  7485  tfrlem16  7489  mapsn  7899  fvdiagfn  7902  mapsnconst  7903  mapsncnv  7904  mapsnf1o2  7905  ralxpmap  7907  elixpsn  7947  ixpsnf1o  7948  mapsnf1o  7949  ensn1  8020  en1b  8024  mapsnen  8035  xpsnen  8044  endisj  8047  xpsnen2g  8053  domunsncan  8060  enfixsn  8069  domunsn  8110  fodomr  8111  disjenex  8118  domssex2  8120  domssex  8121  map2xp  8130  phplem2  8140  isinf  8173  pssnn  8178  findcard2  8200  ac6sfi  8204  xpfi  8231  fodomfi  8239  pwfilem  8260  fczfsuppd  8293  snopfsupp  8298  fisn  8333  marypha1lem  8339  brwdom2  8478  unxpwdom2  8493  elirrv  8504  epfrs  8607  tc2  8618  tcsni  8619  ranksuc  8728  fseqenlem1  8847  dfac5lem2  8947  dfac5lem3  8948  dfac5lem4  8949  kmlem2  8973  cdafn  8991  cdaval  8992  cdaassen  9004  mapcdaen  9006  cdadom1  9008  cdainf  9014  ackbij1lem5  9046  cfsuc  9079  isfin1-3  9208  hsmexlem4  9251  axcc2lem  9258  dcomex  9269  axdc3lem4  9275  axdc4lem  9277  ttukeylem3  9333  brdom7disj  9353  brdom6disj  9354  fpwwe2lem13  9464  canthwe  9473  canthp1lem1  9474  uniwun  9562  rankcf  9599  nn0ex  11298  hashxplem  13220  hashmap  13222  hashbclem  13236  hashf1lem1  13239  hashge3el3dif  13268  ofs1  13709  climconst2  14279  incexclem  14568  ramub1lem2  15731  cshwsex  15807  setsvalg  15887  setsid  15914  pwsbas  16147  pwsle  16152  pwssca  16156  pwssnf1o  16158  imasplusg  16177  imasmulr  16178  imasvsca  16180  imasip  16181  xpsc  16217  acsfn  16320  isfunc  16524  homaf  16680  homaval  16681  funcsetcestrclem1  16794  mgm1  17257  sgrp1  17293  mnd1  17331  mnd1id  17332  grp1  17522  grp1inv  17523  symg2bas  17818  idrespermg  17831  pmtrsn  17939  psgnsn  17940  abl1  18269  gsum2d2  18373  gsumcom2  18374  dprdz  18429  dprdsn  18435  dprd2da  18441  ring1  18602  pwssplit3  19061  drngnidl  19229  drnglpir  19253  rng1nnzr  19274  evlssca  19522  mpfind  19536  evls1sca  19688  pf1ind  19719  frlmip  20117  islindf4  20177  mattposvs  20261  mat1dimelbas  20277  mat1dimscm  20281  mat1dimmul  20282  mat1rhmval  20285  m1detdiag  20403  mdetrlin  20408  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  smadiadetglem2  20478  basdif0  20757  ordtbas  20996  leordtval2  21016  dishaus  21186  discmp  21201  conncompid  21234  dis2ndc  21263  dislly  21300  dis1stc  21302  unisngl  21330  1stckgen  21357  ptbasfi  21384  dfac14lem  21420  dfac14  21421  ptrescn  21442  xkoptsub  21457  pt1hmeo  21609  xpstopnlem1  21612  ptcmpfi  21616  isufil2  21712  ufileu  21723  filufint  21724  uffix  21725  uffixsn  21729  flimclslem  21788  ptcmplem1  21856  cnextfval  21866  imasdsf1olem  22178  icccmplem1  22625  icccmplem2  22626  rrxip  23178  elply2  23952  plyss  23955  plyeq0lem  23966  taylfval  24113  axlowdimlem15  25836  axlowdim  25841  snstriedgval  25930  vtxvalsnop  25933  iedgvalsnop  25934  upgr1eop  26010  upgr1eopALT  26012  uspgr1eop  26139  usgr1eop  26142  lfuhgr1v0e  26146  1loopgrvd2  26399  1loopgrvd0  26400  p1evtxdeqlem  26408  p1evtxdeq  26409  p1evtxdp1  26410  uspgrloopvtx  26411  uspgrloopiedg  26413  uspgrloopedg  26414  wlkp1lem4  26573  0pthonv  26990  eupth2lem3  27096  0ofval  27642  resf1o  29505  ordtconnlem1  29970  esumpr  30128  esumrnmpt2  30130  esumfzf  30131  esum2dlem  30154  esum2d  30155  esumiun  30156  prsiga  30194  rossros  30243  cntnevol  30291  carsgclctunlem1  30379  omsmeas  30385  eulerpartlemgs2  30442  ccatmulgnn0dir  30619  ofcs1  30621  actfunsnf1o  30682  actfunsnrndisj  30683  reprsuc  30693  breprexplema  30708  bnj918  30836  bnj95  30934  bnj1452  31120  bnj1489  31124  subfacp1lem5  31166  erdszelem5  31177  erdszelem8  31180  cvmliftlem4  31270  cvmliftlem5  31271  cvmlift2lem6  31290  cvmlift2lem9  31293  cvmlift2lem12  31296  conway  31910  etasslt  31920  slerec  31923  fobigcup  32007  elsingles  32025  fnsingle  32026  fvsingle  32027  dfiota3  32030  brapply  32045  brsuccf  32048  funpartlem  32049  altopthsn  32068  altxpsspw  32084  hfsn  32286  neibastop2lem  32355  topjoin  32360  onpsstopbas  32429  bj-sels  32950  bj-snsetex  32951  bj-elsngl  32956  bj-2uplex  33010  bj-restsn  33035  bj-snmoore  33068  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  finixpnum  33394  ptrest  33408  poimirlem3  33412  poimirlem4  33413  poimirlem28  33437  fdc  33541  heiborlem3  33612  heiborlem8  33617  ismrer1  33637  grposnOLD  33681  zrdivrng  33752  opideq  34110  ldualset  34412  lineset  35024  ispointN  35028  dvaset  36293  dvhset  36370  dibval  36431  dibfna  36443  elrfi  37257  mzpincl  37297  mzpcompact2lem  37314  wopprc  37597  dfac11  37632  kelac2  37635  pwslnmlem1  37662  pwslnm  37664  fvilbdRP  37982  brtrclfv2  38019  frege110  38267  frege133  38290  k0004lem3  38447  snelpwrVD  39066  fnchoice  39188  mapsnd  39388  mapsnend  39391  mpct  39393  elmapsnd  39396  difmapsn  39404  unirnmapsn  39406  ssmapsn  39408  limcresiooub  39874  limcresioolb  39875  cnfdmsn  40095  dvsinax  40127  fourierdlem48  40371  fourierdlem49  40372  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0sn  40596  sge0p1  40631  sge0xp  40646  ovnovollem1  40870  ovnovollem2  40871  vonvolmbllem  40874  setsv  41348  nnsum3primesprm  41678  mpt2exxg2  42116  mapsnop  42123  lindsrng01  42257  snlindsntorlem  42259  snlindsntor  42260  lmod1lem1  42276  lmod1lem2  42277  lmod1lem3  42278  lmod1lem4  42279  lmod1lem5  42280  lmod1  42281  lmod1zr  42282  aacllem  42547