Theorem snex 5349

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5301. (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 4571	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4668	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 566	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5348	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3495	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	eqeltrid 2843	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4650	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 215	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5226	. . 3 ⊢ ∅ ∈ V
11	9, 10	eqeltrdi 2847	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-pr 4561

This theorem is referenced by:  prex  5350  sels  5351  elALT  5352  dtruALT2  5353  snelpwi  5354  snelpw  5355  rext  5358  sspwb  5359  intid  5367  moabex  5368  nnullss  5371  exss  5372  elopg  5375  opi1  5377  op1stb  5380  opnz  5382  opeqsng  5411  opeqpr  5413  snopeqop  5414  opthwiener  5422  uniop  5423  0sn0ep  5490  frirr  5557  opthprc  5642  frsn  5665  xpsspw  5708  relop  5748  snsn0non  6370  onnev  6372  onnevOLD  6373  funopg  6452  funsneqopb  7006  fsnex  7135  tpex  7575  snnex  7586  difsnexi  7589  sucexb  7631  soex  7742  elxp4  7743  elxp5  7744  fvclex  7775  opabex3d  7781  opabex3rd  7782  opabex3  7783  1stval  7806  2ndval  7807  fo1st  7824  fo2nd  7825  mpoexxg  7889  cnvf1o  7922  fnse  7945  suppsnop  7965  brtpos2  8019  frrlem13  8085  wfrlem15OLD  8125  tfrlem12  8191  tfrlem16  8195  1oex  8280  mapsnd  8632  fvdiagfn  8637  mapsnconst  8638  mapsncnv  8639  mapsnf1o2  8640  ralxpmap  8642  elixpsn  8683  ixpsnf1o  8684  mapsnf1o  8685  ensn1  8761  ensn1OLD  8762  en1bOLD  8768  2dom  8774  mapsnend  8780  snmapen  8782  en2sn  8785  en2snOLD  8786  xpsnen  8796  endisj  8799  xpsnen2g  8805  domunsncan  8812  enfixsn  8821  domunsn  8863  fodomr  8864  disjenex  8871  domssex2  8873  domssex  8874  map2xp  8883  phplem2  8893  findcard2  8909  pssnn  8913  pwfilem  8922  isinf  8965  pssnnOLD  8969  findcard2OLD  8986  ac6sfi  8988  xpfi  9015  fodomfi  9022  pwfilemOLD  9043  fczfsuppd  9076  snopfsupp  9081  fisn  9116  marypha1lem  9122  brwdom2  9262  unxpwdom2  9277  elirrv  9285  epfrs  9420  tc2  9431  tcsni  9432  ranksuc  9554  djuex  9597  fseqenlem1  9711  dfac5lem2  9811  dfac5lem3  9812  dfac5lem4  9813  kmlem2  9838  djuassen  9865  mapdjuen  9867  djudom1  9869  djuinf  9875  ackbij1lem5  9911  cfsuc  9944  isfin1-3  10073  hsmexlem4  10116  axcc2lem  10123  dcomex  10134  axdc3lem4  10140  axdc4lem  10142  ttukeylem3  10198  brdom7disj  10218  brdom6disj  10219  fpwwe2lem12  10329  canthwe  10338  canthp1lem1  10339  uniwun  10427  rankcf  10464  nn0ex  12169  hashxplem  14076  hashmap  14078  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  hashge3el3dif  14128  ofs1  14609  climconst2  15185  incexclem  15476  ramub1lem2  16656  cshwsex  16730  setsvalg  16795  setsid  16837  pwsbas  17115  pwsle  17120  pwssca  17124  pwssnf1o  17126  imasplusg  17145  imasmulr  17146  imasvsca  17148  imasip  17149  acsfn  17285  isfunc  17495  homaf  17661  homaval  17662  funcsetcestrclem1  17787  mgm1  18257  sgrp1  18299  mnd1  18341  mnd1id  18342  efmnd1bas  18447  idresefmnd  18453  smndex1bas  18460  smndex1sgrp  18462  smndex1mnd  18464  smndex1id  18465  grp1  18597  grp1inv  18598  mulgfval  18617  triv1nsgd  18716  1nsgtrivd  18717  symg2bas  18915  symgvalstruct  18919  symgvalstructOLD  18920  idrespermg  18934  pmtrsn  19042  psgnsn  19043  abl1  19382  gsum2d2  19490  gsumcom2  19491  dprdz  19548  dprdsn  19554  dprd2da  19560  simpgnsgd  19618  2nsgsimpgd  19620  ring1  19756  pwssplit3  20238  rng1nnzr  20458  frlmip  20895  islindf4  20955  evlssca  21209  mpfind  21227  evls1sca  21399  pf1ind  21431  mattposvs  21512  mat1dimelbas  21528  mat1dimscm  21532  mat1dimmul  21533  mat1rhmval  21536  m1detdiag  21654  mdetrlin  21659  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  smadiadetglem2  21729  basdif0  22011  ordtbas  22251  leordtval2  22271  dishaus  22441  discmp  22457  conncompid  22490  dis2ndc  22519  dislly  22556  dis1stc  22558  unisngl  22586  1stckgen  22613  ptbasfi  22640  dfac14lem  22676  dfac14  22677  ptrescn  22698  xkoptsub  22713  pt1hmeo  22865  xpstopnlem1  22868  ptcmpfi  22872  isufil2  22967  ufileu  22978  filufint  22979  uffix  22980  uffixsn  22984  flimclslem  23043  ptcmplem1  23111  cnextfval  23121  imasdsf1olem  23434  icccmplem1  23891  icccmplem2  23892  rrxip  24459  rrxsca  24465  ehl1eudis  24489  elply2  25262  plyss  25265  plyeq0lem  25276  taylfval  25423  axlowdimlem15  27227  axlowdim  27232  snstriedgval  27311  vtxvalsnop  27314  iedgvalsnop  27315  upgr1eop  27388  upgr1eopALT  27390  uspgr1eop  27517  usgr1eop  27520  lfuhgr1v0e  27524  1loopgrvd2  27773  1loopgrvd0  27774  p1evtxdeqlem  27782  p1evtxdeq  27783  p1evtxdp1  27784  uspgrloopvtx  27785  uspgrloopiedg  27787  uspgrloopedg  27788  wlkp1lem4  27946  0pthonv  28394  eupth2lem3  28501  wlkl0  28632  0ofval  29050  suppovss  30919  resf1o  30967  gsumpart  31217  zar0ring  31730  ordtconnlem1  31776  esumpr  31934  esumrnmpt2  31936  esumfzf  31937  esum2dlem  31960  esum2d  31961  esumiun  31962  prsiga  31999  rossros  32048  cntnevol  32096  carsgclctunlem1  32184  omsmeas  32190  eulerpartlemgs2  32247  ccatmulgnn0dir  32421  ofcs1  32423  actfunsnf1o  32484  actfunsnrndisj  32485  reprsuc  32495  breprexplema  32510  bnj918  32646  bnj95  32744  bnj1452  32932  bnj1489  32936  fineqvac  32966  subfacp1lem5  33046  erdszelem5  33057  erdszelem8  33060  cvmliftlem4  33150  cvmliftlem5  33151  cvmlift2lem6  33170  cvmlift2lem9  33173  cvmlift2lem12  33176  satfv1lem  33224  prv1n  33293  sexp2  33720  sexp3  33726  naddcllem  33758  conway  33920  etasslt  33934  slerec  33940  0slt1s  33950  ssltleft  33981  ssltright  33982  cofcutr  34019  addsval  34053  fobigcup  34129  elsingles  34147  fnsingle  34148  fvsingle  34149  dfiota3  34152  brapply  34167  brsuccf  34170  funpartlem  34171  altopthsn  34190  altxpsspw  34206  hfsn  34408  neibastop2lem  34476  topjoin  34481  onpsstopbas  34546  bj-snsetex  35080  bj-elsngl  35085  bj-2uplex  35139  bj-restsn  35180  f1omptsnlem  35434  mptsnunlem  35436  topdifinffinlem  35445  finixpnum  35689  ptrest  35703  poimirlem3  35707  poimirlem4  35708  poimirlem28  35732  fdc  35830  heiborlem3  35898  heiborlem8  35903  ismrer1  35923  grposnOLD  35967  zrdivrng  36038  ecexALTV  36393  eccnvepex  36397  ldualset  37066  lineset  37679  ispointN  37683  dvaset  38946  dvhset  39022  dibval  39083  dibfna  39095  sticksstones9  40038  frlmsnic  40188  evlsbagval  40198  elrfi  40432  mzpincl  40472  mzpcompact2lem  40489  wopprc  40768  dfac11  40803  kelac2  40806  pwslnmlem1  40833  pwslnm  40835  sn1dom  41031  pr2dom  41032  tr3dom  41033  fvilbdRP  41187  brtrclfv2  41224  frege110  41470  frege133  41493  k0004lem3  41648  mnuprdlem1  41779  mnuprdlem2  41780  snelpwrVD  42340  fnchoice  42461  mpct  42630  elmapsnd  42633  difmapsn  42641  unirnmapsn  42643  ssmapsn  42645  limcresiooub  43073  limcresioolb  43074  cnfdmsn  43313  dvsinax  43344  fourierdlem48  43585  fourierdlem49  43586  salexct3  43771  salgencntex  43772  salgensscntex  43773  sge0sn  43807  sge0p1  43842  sge0xp  43857  ovnovollem1  44084  ovnovollem2  44085  vonvolmbllem  44088  fsetsnf  44432  fsetsnf1  44433  fsetsnfo  44434  cfsetsnfsetfo  44441  setsv  44718  nnsum3primesprm  45130  mpoexxg2  45561  mapsnop  45568  lindsrng01  45697  snlindsntorlem  45699  snlindsntor  45700  lmod1lem1  45716  lmod1lem2  45717  lmod1lem3  45718  lmod1lem4  45719  lmod1lem5  45720  lmod1  45721  lmod1zr  45722  fv1arycl  45871  1arympt1fv  45873  1arymaptfo  45877  eufsn2  46058  prstchomval  46241  mndtcbasval  46253  mndtchom  46257  mndtcco  46258  aacllem  46391