Theorem snex 5332

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5284. (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 4580	. . 3 ⊢ {𝐴} = {𝐴, 𝐴}
2		preq12 4671	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 569	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2897	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5331	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3567	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	eqeltrid 2917	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4653	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 218	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5211	. . 3 ⊢ ∅ ∈ V
11	9, 10	eqeltrdi 2921	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 184	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2114  Vcvv 3494  ∅c0 4291  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-nul 4292  df-sn 4568  df-pr 4570

This theorem is referenced by:  prex  5333  sels  5334  elALT  5335  dtruALT2  5336  snelpwi  5337  snelpw  5338  rext  5341  sspwb  5342  intid  5350  moabex  5351  nnullss  5354  exss  5355  elopg  5358  opi1  5360  op1stb  5363  opnz  5365  opeqsng  5393  opeqpr  5395  snopeqop  5396  opthwiener  5404  uniop  5405  0sn0ep  5470  frirr  5532  opthprc  5616  frsn  5639  xpsspw  5682  relop  5721  snsn0non  6309  onnev  6311  funopg  6389  funsneqopb  6914  fsnex  7039  tpex  7470  snnex  7480  difsnexi  7483  sucexb  7524  soex  7626  elxp4  7627  elxp5  7628  fvclex  7660  opabex3d  7666  opabex3rd  7667  opabex3  7668  1stval  7691  2ndval  7692  fo1st  7709  fo2nd  7710  mpoexxg  7773  cnvf1o  7806  fnse  7827  suppsnop  7844  brtpos2  7898  wfrlem15  7969  tfrlem12  8025  tfrlem16  8029  mapsnd  8450  fvdiagfn  8455  mapsnconst  8456  mapsncnv  8457  mapsnf1o2  8458  ralxpmap  8460  elixpsn  8501  ixpsnf1o  8502  mapsnf1o  8503  ensn1  8573  en1b  8577  2dom  8582  mapsnend  8588  snmapen  8590  xpsnen  8601  endisj  8604  xpsnen2g  8610  domunsncan  8617  enfixsn  8626  domunsn  8667  fodomr  8668  disjenex  8675  domssex2  8677  domssex  8678  map2xp  8687  phplem2  8697  isinf  8731  pssnn  8736  findcard2  8758  ac6sfi  8762  xpfi  8789  fodomfi  8797  pwfilem  8818  fczfsuppd  8851  snopfsupp  8856  fisn  8891  marypha1lem  8897  brwdom2  9037  unxpwdom2  9052  elirrv  9060  epfrs  9173  tc2  9184  tcsni  9185  ranksuc  9294  djuex  9337  fseqenlem1  9450  dfac5lem2  9550  dfac5lem3  9551  dfac5lem4  9552  kmlem2  9577  djuassen  9604  mapdjuen  9606  djudom1  9608  djuinf  9614  ackbij1lem5  9646  cfsuc  9679  isfin1-3  9808  hsmexlem4  9851  axcc2lem  9858  dcomex  9869  axdc3lem4  9875  axdc4lem  9877  ttukeylem3  9933  brdom7disj  9953  brdom6disj  9954  fpwwe2lem13  10064  canthwe  10073  canthp1lem1  10074  uniwun  10162  rankcf  10199  nn0ex  11904  hashxplem  13795  hashmap  13797  hashbclem  13811  hashf1lem1  13814  hashge3el3dif  13845  ofs1  14330  climconst2  14905  incexclem  15191  ramub1lem2  16363  cshwsex  16434  setsvalg  16512  setsid  16538  pwsbas  16760  pwsle  16765  pwssca  16769  pwssnf1o  16771  imasplusg  16790  imasmulr  16791  imasvsca  16793  imasip  16794  acsfn  16930  isfunc  17134  homaf  17290  homaval  17291  funcsetcestrclem1  17404  mgm1  17868  sgrp1  17910  mnd1  17952  mnd1id  17953  efmnd1bas  18058  idresefmnd  18064  smndex1bas  18071  smndex1sgrp  18073  smndex1mnd  18075  smndex1id  18076  grp1  18206  grp1inv  18207  mulgfval  18226  triv1nsgd  18325  1nsgtrivd  18326  symg2bas  18521  symgvalstruct  18525  idrespermg  18539  pmtrsn  18647  psgnsn  18648  abl1  18986  gsum2d2  19094  gsumcom2  19095  dprdz  19152  dprdsn  19158  dprd2da  19164  simpgnsgd  19222  2nsgsimpgd  19224  ring1  19352  pwssplit3  19833  rng1nnzr  20047  evlssca  20302  mpfind  20320  evls1sca  20486  pf1ind  20518  frlmip  20922  islindf4  20982  mattposvs  21064  mat1dimelbas  21080  mat1dimscm  21084  mat1dimmul  21085  mat1rhmval  21088  m1detdiag  21206  mdetrlin  21211  mdetrsca2  21213  mdetrlin2  21216  mdetunilem5  21225  smadiadetglem2  21281  basdif0  21561  ordtbas  21800  leordtval2  21820  dishaus  21990  discmp  22006  conncompid  22039  dis2ndc  22068  dislly  22105  dis1stc  22107  unisngl  22135  1stckgen  22162  ptbasfi  22189  dfac14lem  22225  dfac14  22226  ptrescn  22247  xkoptsub  22262  pt1hmeo  22414  xpstopnlem1  22417  ptcmpfi  22421  isufil2  22516  ufileu  22527  filufint  22528  uffix  22529  uffixsn  22533  flimclslem  22592  ptcmplem1  22660  cnextfval  22670  imasdsf1olem  22983  icccmplem1  23430  icccmplem2  23431  rrxip  23993  rrxsca  23999  ehl1eudis  24023  elply2  24786  plyss  24789  plyeq0lem  24800  taylfval  24947  axlowdimlem15  26742  axlowdim  26747  snstriedgval  26823  vtxvalsnop  26826  iedgvalsnop  26827  upgr1eop  26900  upgr1eopALT  26902  uspgr1eop  27029  usgr1eop  27032  lfuhgr1v0e  27036  1loopgrvd2  27285  1loopgrvd0  27286  p1evtxdeqlem  27294  p1evtxdeq  27295  p1evtxdp1  27296  uspgrloopvtx  27297  uspgrloopiedg  27299  uspgrloopedg  27300  wlkp1lem4  27458  0pthonv  27908  eupth2lem3  28015  wlkl0  28146  0ofval  28564  suppovss  30426  resf1o  30466  ordtconnlem1  31167  esumpr  31325  esumrnmpt2  31327  esumfzf  31328  esum2dlem  31351  esum2d  31352  esumiun  31353  prsiga  31390  rossros  31439  cntnevol  31487  carsgclctunlem1  31575  omsmeas  31581  eulerpartlemgs2  31638  ccatmulgnn0dir  31812  ofcs1  31814  actfunsnf1o  31875  actfunsnrndisj  31876  reprsuc  31886  breprexplema  31901  bnj918  32037  bnj95  32136  bnj1452  32324  bnj1489  32328  subfacp1lem5  32431  erdszelem5  32442  erdszelem8  32445  cvmliftlem4  32535  cvmliftlem5  32536  cvmlift2lem6  32555  cvmlift2lem9  32558  cvmlift2lem12  32561  satfv1lem  32609  prv1n  32678  frrlem13  33135  conway  33264  etasslt  33274  slerec  33277  fobigcup  33361  elsingles  33379  fnsingle  33380  fvsingle  33381  dfiota3  33384  brapply  33399  brsuccf  33402  funpartlem  33403  altopthsn  33422  altxpsspw  33438  hfsn  33640  neibastop2lem  33708  topjoin  33713  onpsstopbas  33778  bj-snsetex  34278  bj-elsngl  34283  bj-2uplex  34337  bj-restsn  34376  f1omptsnlem  34620  mptsnunlem  34622  topdifinffinlem  34631  finixpnum  34892  ptrest  34906  poimirlem3  34910  poimirlem4  34911  poimirlem28  34935  fdc  35035  heiborlem3  35106  heiborlem8  35111  ismrer1  35131  grposnOLD  35175  zrdivrng  35246  ecexALTV  35603  eccnvepex  35607  ldualset  36276  lineset  36889  ispointN  36893  dvaset  38156  dvhset  38232  dibval  38293  dibfna  38305  frlmsnic  39169  elrfi  39311  mzpincl  39351  mzpcompact2lem  39368  wopprc  39647  dfac11  39682  kelac2  39685  pwslnmlem1  39712  pwslnm  39714  sn1dom  39912  pr2dom  39913  tr3dom  39914  fvilbdRP  40055  brtrclfv2  40092  frege110  40339  frege133  40362  k0004lem3  40519  mnuprdlem1  40628  mnuprdlem2  40629  snelpwrVD  41185  fnchoice  41306  mpct  41484  elmapsnd  41487  difmapsn  41495  unirnmapsn  41497  ssmapsn  41499  limcresiooub  41943  limcresioolb  41944  cnfdmsn  42185  dvsinax  42217  fourierdlem48  42459  fourierdlem49  42460  salexct3  42645  salgencntex  42646  salgensscntex  42647  sge0sn  42681  sge0p1  42716  sge0xp  42731  ovnovollem1  42958  ovnovollem2  42959  vonvolmbllem  42962  setsv  43558  nnsum3primesprm  43975  mpoexxg2  44406  mapsnop  44413  lindsrng01  44543  snlindsntorlem  44545  snlindsntor  44546  lmod1lem1  44562  lmod1lem2  44563  lmod1lem3  44564  lmod1lem4  44565  lmod1lem5  44566  lmod1  44567  lmod1zr  44568  aacllem  44922