Theorem snex 5354

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5306. (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 4574	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4671	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 567	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2823	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5353	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3505	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	eqeltrid 2843	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4653	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 215	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5231	. . 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 2106  Vcvv 3432  ∅c0 4256  {csn 4561  {cpr 4563

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-sn 4562  df-pr 4564

This theorem is referenced by:  prex  5355  sels  5356  elALT  5358  snelpwi  5360  snelpw  5361  rext  5364  sspwb  5365  intid  5373  moabex  5374  nnullss  5377  exss  5378  elopg  5381  opi1  5383  op1stb  5386  opnz  5388  opeqsng  5417  opeqpr  5419  snopeqop  5420  opthwiener  5428  uniop  5429  0sn0ep  5499  frirr  5566  opthprc  5651  frsn  5674  xpsspw  5719  relop  5759  snsn0non  6385  onnev  6387  onnevOLD  6388  funopg  6468  funsneqopb  7024  fsnex  7155  tpex  7597  snnex  7608  difsnexi  7611  sucexb  7654  soex  7768  elxp4  7769  elxp5  7770  fvclex  7801  opabex3d  7808  opabex3rd  7809  opabex3  7810  1stval  7833  2ndval  7834  fo1st  7851  fo2nd  7852  mpoexxg  7916  cnvf1o  7951  fnse  7974  suppsnop  7994  brtpos2  8048  frrlem13  8114  wfrlem15OLD  8154  tfrlem12  8220  tfrlem16  8224  1oex  8307  mapsnd  8674  fvdiagfn  8679  mapsnconst  8680  mapsncnv  8681  mapsnf1o2  8682  ralxpmap  8684  elixpsn  8725  ixpsnf1o  8726  mapsnf1o  8727  ensn1  8807  ensn1OLD  8808  en1bOLD  8814  2dom  8820  mapsnend  8826  snmapen  8828  en2sn  8831  en2snOLD  8832  xpsnen  8842  endisj  8845  xpsnen2g  8852  domunsncan  8859  enfixsn  8868  domunsn  8914  fodomr  8915  disjenex  8922  domssex2  8924  domssex  8925  map2xp  8934  findcard2  8947  pssnn  8951  pwfilem  8960  phplem2OLD  9001  snnen2o  9026  isinf  9036  pssnnOLD  9040  findcard2OLD  9056  ac6sfi  9058  xpfi  9085  fodomfi  9092  pwfilemOLD  9113  fczfsuppd  9146  snopfsupp  9151  fisn  9186  marypha1lem  9192  brwdom2  9332  unxpwdom2  9347  elirrv  9355  epfrs  9489  tc2  9500  tcsni  9501  ranksuc  9623  djuex  9666  fseqenlem1  9780  dfac5lem2  9880  dfac5lem3  9881  dfac5lem4  9882  kmlem2  9907  djuassen  9934  mapdjuen  9936  djudom1  9938  djuinf  9944  ackbij1lem5  9980  cfsuc  10013  isfin1-3  10142  hsmexlem4  10185  axcc2lem  10192  dcomex  10203  axdc3lem4  10209  axdc4lem  10211  ttukeylem3  10267  brdom7disj  10287  brdom6disj  10288  fpwwe2lem12  10398  canthwe  10407  canthp1lem1  10408  uniwun  10496  rankcf  10533  nn0ex  12239  hashxplem  14148  hashmap  14150  hashbclem  14164  hashf1lem1  14168  hashf1lem1OLD  14169  hashge3el3dif  14200  ofs1  14681  climconst2  15257  incexclem  15548  ramub1lem2  16728  cshwsex  16802  setsvalg  16867  setsid  16909  pwsbas  17198  pwsle  17203  pwssca  17207  pwssnf1o  17209  imasplusg  17228  imasmulr  17229  imasvsca  17231  imasip  17232  acsfn  17368  isfunc  17579  homaf  17745  homaval  17746  funcsetcestrclem1  17871  mgm1  18342  sgrp1  18384  mnd1  18426  mnd1id  18427  efmnd1bas  18532  idresefmnd  18538  smndex1bas  18545  smndex1sgrp  18547  smndex1mnd  18549  smndex1id  18550  grp1  18682  grp1inv  18683  mulgfval  18702  triv1nsgd  18801  1nsgtrivd  18802  symg2bas  19000  symgvalstruct  19004  symgvalstructOLD  19005  idrespermg  19019  pmtrsn  19127  psgnsn  19128  abl1  19467  gsum2d2  19575  gsumcom2  19576  dprdz  19633  dprdsn  19639  dprd2da  19645  simpgnsgd  19703  2nsgsimpgd  19705  ring1  19841  pwssplit3  20323  rng1nnzr  20545  frlmip  20985  islindf4  21045  evlssca  21299  mpfind  21317  evls1sca  21489  pf1ind  21521  mattposvs  21604  mat1dimelbas  21620  mat1dimscm  21624  mat1dimmul  21625  mat1rhmval  21628  m1detdiag  21746  mdetrlin  21751  mdetrsca2  21753  mdetrlin2  21756  mdetunilem5  21765  smadiadetglem2  21821  basdif0  22103  ordtbas  22343  leordtval2  22363  dishaus  22533  discmp  22549  conncompid  22582  dis2ndc  22611  dislly  22648  dis1stc  22650  unisngl  22678  1stckgen  22705  ptbasfi  22732  dfac14lem  22768  dfac14  22769  ptrescn  22790  xkoptsub  22805  pt1hmeo  22957  xpstopnlem1  22960  ptcmpfi  22964  isufil2  23059  ufileu  23070  filufint  23071  uffix  23072  uffixsn  23076  flimclslem  23135  ptcmplem1  23203  cnextfval  23213  imasdsf1olem  23526  icccmplem1  23985  icccmplem2  23986  rrxip  24554  rrxsca  24560  ehl1eudis  24584  elply2  25357  plyss  25360  plyeq0lem  25371  taylfval  25518  axlowdimlem15  27324  axlowdim  27329  snstriedgval  27408  vtxvalsnop  27411  iedgvalsnop  27412  upgr1eop  27485  upgr1eopALT  27487  uspgr1eop  27614  usgr1eop  27617  lfuhgr1v0e  27621  1loopgrvd2  27870  1loopgrvd0  27871  p1evtxdeqlem  27879  p1evtxdeq  27880  p1evtxdp1  27881  uspgrloopvtx  27882  uspgrloopiedg  27884  uspgrloopedg  27885  wlkp1lem4  28044  0pthonv  28493  eupth2lem3  28600  wlkl0  28731  0ofval  29149  suppovss  31017  resf1o  31065  gsumpart  31315  zar0ring  31828  ordtconnlem1  31874  esumpr  32034  esumrnmpt2  32036  esumfzf  32037  esum2dlem  32060  esum2d  32061  esumiun  32062  prsiga  32099  rossros  32148  cntnevol  32196  carsgclctunlem1  32284  omsmeas  32290  eulerpartlemgs2  32347  ccatmulgnn0dir  32521  ofcs1  32523  actfunsnf1o  32584  actfunsnrndisj  32585  reprsuc  32595  breprexplema  32610  bnj918  32746  bnj95  32844  bnj1452  33032  bnj1489  33036  fineqvac  33066  subfacp1lem5  33146  erdszelem5  33157  erdszelem8  33160  cvmliftlem4  33250  cvmliftlem5  33251  cvmlift2lem6  33270  cvmlift2lem9  33273  cvmlift2lem12  33276  satfv1lem  33324  prv1n  33393  sexp2  33793  sexp3  33799  naddcllem  33831  conway  33993  etasslt  34007  slerec  34013  0slt1s  34023  ssltleft  34054  ssltright  34055  cofcutr  34092  addsval  34126  fobigcup  34202  elsingles  34220  fnsingle  34221  fvsingle  34222  dfiota3  34225  brapply  34240  brsuccf  34243  funpartlem  34244  altopthsn  34263  altxpsspw  34279  hfsn  34481  neibastop2lem  34549  topjoin  34554  onpsstopbas  34619  bj-snsetex  35153  bj-elsngl  35158  bj-2uplex  35212  bj-restsn  35253  f1omptsnlem  35507  mptsnunlem  35509  topdifinffinlem  35518  finixpnum  35762  ptrest  35776  poimirlem3  35780  poimirlem4  35781  poimirlem28  35805  fdc  35903  heiborlem3  35971  heiborlem8  35976  ismrer1  35996  grposnOLD  36040  zrdivrng  36111  ecexALTV  36466  eccnvepex  36470  ldualset  37139  lineset  37752  ispointN  37756  dvaset  39019  dvhset  39095  dibval  39156  dibfna  39168  sticksstones9  40110  frlmsnic  40263  evlsbagval  40275  elrfi  40516  mzpincl  40556  mzpcompact2lem  40573  wopprc  40852  dfac11  40887  kelac2  40890  pwslnmlem1  40917  pwslnm  40919  sn1dom  41133  pr2dom  41134  tr3dom  41135  fvilbdRP  41298  brtrclfv2  41335  frege110  41581  frege133  41604  k0004lem3  41759  mnuprdlem1  41890  mnuprdlem2  41891  snelpwrVD  42451  fnchoice  42572  mpct  42741  elmapsnd  42744  difmapsn  42752  unirnmapsn  42754  ssmapsn  42756  limcresiooub  43183  limcresioolb  43184  cnfdmsn  43423  dvsinax  43454  fourierdlem48  43695  fourierdlem49  43696  salexct3  43881  salgencntex  43882  salgensscntex  43883  sge0sn  43917  sge0p1  43952  sge0xp  43967  ovnovollem1  44194  ovnovollem2  44195  vonvolmbllem  44198  fsetsnf  44545  fsetsnf1  44546  fsetsnfo  44547  cfsetsnfsetfo  44554  setsv  44830  nnsum3primesprm  45242  mpoexxg2  45673  mapsnop  45680  lindsrng01  45809  snlindsntorlem  45811  snlindsntor  45812  lmod1lem1  45828  lmod1lem2  45829  lmod1lem3  45830  lmod1lem4  45831  lmod1lem5  45832  lmod1  45833  lmod1zr  45834  fv1arycl  45983  1arympt1fv  45985  1arymaptfo  45989  eufsn2  46170  prstchomval  46355  mndtcbasval  46367  mndtchom  46371  mndtcco  46372  aacllem  46505