Theorem snex 5309

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5261. (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 4540	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4637	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 570	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2815	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5308	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3471	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	eqeltrid 2835	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4619	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 219	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5185	. . 3 ⊢ ∅ ∈ V
11	9, 10	eqeltrdi 2839	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 185	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1543   ∈ wcel 2112  Vcvv 3398  ∅c0 4223  {csn 4527  {cpr 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-sn 4528  df-pr 4530

This theorem is referenced by:  prex  5310  sels  5311  elALT  5312  dtruALT2  5313  snelpwi  5314  snelpw  5315  rext  5318  sspwb  5319  intid  5327  moabex  5328  nnullss  5331  exss  5332  elopg  5335  opi1  5337  op1stb  5340  opnz  5342  opeqsng  5371  opeqpr  5373  snopeqop  5374  opthwiener  5382  uniop  5383  0sn0ep  5449  frirr  5513  opthprc  5598  frsn  5621  xpsspw  5664  relop  5704  snsn0non  6310  onnev  6312  onnevOLD  6313  funopg  6392  funsneqopb  6945  fsnex  7071  tpex  7510  snnex  7521  difsnexi  7524  sucexb  7566  soex  7677  elxp4  7678  elxp5  7679  fvclex  7710  opabex3d  7716  opabex3rd  7717  opabex3  7718  1stval  7741  2ndval  7742  fo1st  7759  fo2nd  7760  mpoexxg  7824  cnvf1o  7857  fnse  7878  suppsnop  7898  brtpos2  7952  frrlem13  8017  wfrlem15  8047  tfrlem12  8103  tfrlem16  8107  1oex  8193  mapsnd  8545  fvdiagfn  8550  mapsnconst  8551  mapsncnv  8552  mapsnf1o2  8553  ralxpmap  8555  elixpsn  8596  ixpsnf1o  8597  mapsnf1o  8598  ensn1  8672  ensn1OLD  8673  en1bOLD  8679  2dom  8685  mapsnend  8691  snmapen  8693  en2sn  8696  en2snOLD  8697  xpsnen  8707  endisj  8710  xpsnen2g  8716  domunsncan  8723  enfixsn  8732  domunsn  8774  fodomr  8775  disjenex  8782  domssex2  8784  domssex  8785  map2xp  8794  phplem2  8804  findcard2  8820  pssnn  8824  pwfilem  8832  isinf  8867  pssnnOLD  8872  findcard2OLD  8891  ac6sfi  8893  xpfi  8920  fodomfi  8927  pwfilemOLD  8948  fczfsuppd  8981  snopfsupp  8986  fisn  9021  marypha1lem  9027  brwdom2  9167  unxpwdom2  9182  elirrv  9190  epfrs  9325  tc2  9336  tcsni  9337  ranksuc  9446  djuex  9489  fseqenlem1  9603  dfac5lem2  9703  dfac5lem3  9704  dfac5lem4  9705  kmlem2  9730  djuassen  9757  mapdjuen  9759  djudom1  9761  djuinf  9767  ackbij1lem5  9803  cfsuc  9836  isfin1-3  9965  hsmexlem4  10008  axcc2lem  10015  dcomex  10026  axdc3lem4  10032  axdc4lem  10034  ttukeylem3  10090  brdom7disj  10110  brdom6disj  10111  fpwwe2lem12  10221  canthwe  10230  canthp1lem1  10231  uniwun  10319  rankcf  10356  nn0ex  12061  hashxplem  13965  hashmap  13967  hashbclem  13981  hashf1lem1  13985  hashf1lem1OLD  13986  hashge3el3dif  14017  ofs1  14498  climconst2  15074  incexclem  15363  ramub1lem2  16543  cshwsex  16617  setsvalg  16694  setsid  16719  pwsbas  16946  pwsle  16951  pwssca  16955  pwssnf1o  16957  imasplusg  16976  imasmulr  16977  imasvsca  16979  imasip  16980  acsfn  17116  isfunc  17324  homaf  17490  homaval  17491  funcsetcestrclem1  17615  mgm1  18084  sgrp1  18126  mnd1  18168  mnd1id  18169  efmnd1bas  18274  idresefmnd  18280  smndex1bas  18287  smndex1sgrp  18289  smndex1mnd  18291  smndex1id  18292  grp1  18424  grp1inv  18425  mulgfval  18444  triv1nsgd  18543  1nsgtrivd  18544  symg2bas  18739  symgvalstruct  18743  idrespermg  18757  pmtrsn  18865  psgnsn  18866  abl1  19205  gsum2d2  19313  gsumcom2  19314  dprdz  19371  dprdsn  19377  dprd2da  19383  simpgnsgd  19441  2nsgsimpgd  19443  ring1  19574  pwssplit3  20052  rng1nnzr  20266  frlmip  20694  islindf4  20754  evlssca  21003  mpfind  21021  evls1sca  21193  pf1ind  21225  mattposvs  21306  mat1dimelbas  21322  mat1dimscm  21326  mat1dimmul  21327  mat1rhmval  21330  m1detdiag  21448  mdetrlin  21453  mdetrsca2  21455  mdetrlin2  21458  mdetunilem5  21467  smadiadetglem2  21523  basdif0  21804  ordtbas  22043  leordtval2  22063  dishaus  22233  discmp  22249  conncompid  22282  dis2ndc  22311  dislly  22348  dis1stc  22350  unisngl  22378  1stckgen  22405  ptbasfi  22432  dfac14lem  22468  dfac14  22469  ptrescn  22490  xkoptsub  22505  pt1hmeo  22657  xpstopnlem1  22660  ptcmpfi  22664  isufil2  22759  ufileu  22770  filufint  22771  uffix  22772  uffixsn  22776  flimclslem  22835  ptcmplem1  22903  cnextfval  22913  imasdsf1olem  23225  icccmplem1  23673  icccmplem2  23674  rrxip  24241  rrxsca  24247  ehl1eudis  24271  elply2  25044  plyss  25047  plyeq0lem  25058  taylfval  25205  axlowdimlem15  27001  axlowdim  27006  snstriedgval  27083  vtxvalsnop  27086  iedgvalsnop  27087  upgr1eop  27160  upgr1eopALT  27162  uspgr1eop  27289  usgr1eop  27292  lfuhgr1v0e  27296  1loopgrvd2  27545  1loopgrvd0  27546  p1evtxdeqlem  27554  p1evtxdeq  27555  p1evtxdp1  27556  uspgrloopvtx  27557  uspgrloopiedg  27559  uspgrloopedg  27560  wlkp1lem4  27718  0pthonv  28166  eupth2lem3  28273  wlkl0  28404  0ofval  28822  suppovss  30691  resf1o  30739  gsumpart  30988  zar0ring  31496  ordtconnlem1  31542  esumpr  31700  esumrnmpt2  31702  esumfzf  31703  esum2dlem  31726  esum2d  31727  esumiun  31728  prsiga  31765  rossros  31814  cntnevol  31862  carsgclctunlem1  31950  omsmeas  31956  eulerpartlemgs2  32013  ccatmulgnn0dir  32187  ofcs1  32189  actfunsnf1o  32250  actfunsnrndisj  32251  reprsuc  32261  breprexplema  32276  bnj918  32412  bnj95  32511  bnj1452  32699  bnj1489  32703  fineqvac  32733  subfacp1lem5  32813  erdszelem5  32824  erdszelem8  32827  cvmliftlem4  32917  cvmliftlem5  32918  cvmlift2lem6  32937  cvmlift2lem9  32940  cvmlift2lem12  32943  satfv1lem  32991  prv1n  33060  sexp2  33473  sexp3  33479  naddcllem  33517  conway  33679  etasslt  33693  slerec  33699  0slt1s  33709  ssltleft  33740  ssltright  33741  cofcutr  33778  addsval  33812  fobigcup  33888  elsingles  33906  fnsingle  33907  fvsingle  33908  dfiota3  33911  brapply  33926  brsuccf  33929  funpartlem  33930  altopthsn  33949  altxpsspw  33965  hfsn  34167  neibastop2lem  34235  topjoin  34240  onpsstopbas  34305  bj-snsetex  34839  bj-elsngl  34844  bj-2uplex  34898  bj-restsn  34937  f1omptsnlem  35193  mptsnunlem  35195  topdifinffinlem  35204  finixpnum  35448  ptrest  35462  poimirlem3  35466  poimirlem4  35467  poimirlem28  35491  fdc  35589  heiborlem3  35657  heiborlem8  35662  ismrer1  35682  grposnOLD  35726  zrdivrng  35797  ecexALTV  36152  eccnvepex  36156  ldualset  36825  lineset  37438  ispointN  37442  dvaset  38705  dvhset  38781  dibval  38842  dibfna  38854  sticksstones9  39779  frlmsnic  39916  evlsbagval  39926  elrfi  40160  mzpincl  40200  mzpcompact2lem  40217  wopprc  40496  dfac11  40531  kelac2  40534  pwslnmlem1  40561  pwslnm  40563  sn1dom  40759  pr2dom  40760  tr3dom  40761  fvilbdRP  40916  brtrclfv2  40953  frege110  41199  frege133  41222  k0004lem3  41377  mnuprdlem1  41504  mnuprdlem2  41505  snelpwrVD  42065  fnchoice  42186  mpct  42355  elmapsnd  42358  difmapsn  42366  unirnmapsn  42368  ssmapsn  42370  limcresiooub  42801  limcresioolb  42802  cnfdmsn  43041  dvsinax  43072  fourierdlem48  43313  fourierdlem49  43314  salexct3  43499  salgencntex  43500  salgensscntex  43501  sge0sn  43535  sge0p1  43570  sge0xp  43585  ovnovollem1  43812  ovnovollem2  43813  vonvolmbllem  43816  fsetsnf  44160  fsetsnf1  44161  fsetsnfo  44162  cfsetsnfsetfo  44169  setsv  44446  nnsum3primesprm  44858  mpoexxg2  45289  mapsnop  45296  lindsrng01  45425  snlindsntorlem  45427  snlindsntor  45428  lmod1lem1  45444  lmod1lem2  45445  lmod1lem3  45446  lmod1lem4  45447  lmod1lem5  45448  lmod1  45449  lmod1zr  45450  fv1arycl  45599  1arympt1fv  45601  1arymaptfo  45605  eufsn2  45786  prstchomval  45969  mndtcbasval  45981  mndtchom  45985  mndtcco  45986  aacllem  46119