Theorem snex 5358

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5310. (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 4677	. . . . . 6 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
3	2	anidms 567	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
4	3	eleq1d 2825	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5		zfpair2 5357	. . . 4 ⊢ {𝑥, 𝑥} ∈ V
6	4, 5	vtoclg 3504	. . 3 ⊢ (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
7	1, 6	eqeltrid 2845	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
8		snprc 4659	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9	8	biimpi 215	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
10		0ex 5235	. . 3 ⊢ ∅ ∈ V
11	9, 10	eqeltrdi 2849	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
12	7, 11	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2110  Vcvv 3431  ∅c0 4262  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-sn 4568  df-pr 4570

This theorem is referenced by:  prex  5359  sels  5360  elALT  5362  snelpwi  5364  snelpw  5365  rext  5368  sspwb  5369  intid  5377  moabex  5378  nnullss  5381  exss  5382  elopg  5385  opi1  5387  op1stb  5390  opnz  5392  opeqsng  5421  opeqpr  5423  snopeqop  5424  opthwiener  5432  uniop  5433  0sn0ep  5500  frirr  5567  opthprc  5652  frsn  5675  xpsspw  5718  relop  5758  snsn0non  6384  onnev  6386  onnevOLD  6387  funopg  6466  funsneqopb  7021  fsnex  7151  tpex  7591  snnex  7602  difsnexi  7605  sucexb  7648  soex  7762  elxp4  7763  elxp5  7764  fvclex  7795  opabex3d  7801  opabex3rd  7802  opabex3  7803  1stval  7826  2ndval  7827  fo1st  7844  fo2nd  7845  mpoexxg  7909  cnvf1o  7942  fnse  7965  suppsnop  7985  brtpos2  8039  frrlem13  8105  wfrlem15OLD  8145  tfrlem12  8211  tfrlem16  8215  1oex  8298  mapsnd  8657  fvdiagfn  8662  mapsnconst  8663  mapsncnv  8664  mapsnf1o2  8665  ralxpmap  8667  elixpsn  8708  ixpsnf1o  8709  mapsnf1o  8710  ensn1  8790  ensn1OLD  8791  en1bOLD  8797  2dom  8803  mapsnend  8809  snmapen  8811  en2sn  8814  en2snOLD  8815  xpsnen  8825  endisj  8828  xpsnen2g  8834  domunsncan  8841  enfixsn  8850  domunsn  8896  fodomr  8897  disjenex  8904  domssex2  8906  domssex  8907  map2xp  8916  findcard2  8929  pssnn  8933  pwfilem  8942  phplem2OLD  8983  isinf  9014  pssnnOLD  9018  findcard2OLD  9034  ac6sfi  9036  xpfi  9063  fodomfi  9070  pwfilemOLD  9091  fczfsuppd  9124  snopfsupp  9129  fisn  9164  marypha1lem  9170  brwdom2  9310  unxpwdom2  9325  elirrv  9333  epfrs  9489  tc2  9500  tcsni  9501  ranksuc  9624  djuex  9667  fseqenlem1  9781  dfac5lem2  9881  dfac5lem3  9882  dfac5lem4  9883  kmlem2  9908  djuassen  9935  mapdjuen  9937  djudom1  9939  djuinf  9945  ackbij1lem5  9981  cfsuc  10014  isfin1-3  10143  hsmexlem4  10186  axcc2lem  10193  dcomex  10204  axdc3lem4  10210  axdc4lem  10212  ttukeylem3  10268  brdom7disj  10288  brdom6disj  10289  fpwwe2lem12  10399  canthwe  10408  canthp1lem1  10409  uniwun  10497  rankcf  10534  nn0ex  12239  hashxplem  14146  hashmap  14148  hashbclem  14162  hashf1lem1  14166  hashf1lem1OLD  14167  hashge3el3dif  14198  ofs1  14679  climconst2  15255  incexclem  15546  ramub1lem2  16726  cshwsex  16800  setsvalg  16865  setsid  16907  pwsbas  17196  pwsle  17201  pwssca  17205  pwssnf1o  17207  imasplusg  17226  imasmulr  17227  imasvsca  17229  imasip  17230  acsfn  17366  isfunc  17577  homaf  17743  homaval  17744  funcsetcestrclem1  17869  mgm1  18340  sgrp1  18382  mnd1  18424  mnd1id  18425  efmnd1bas  18530  idresefmnd  18536  smndex1bas  18543  smndex1sgrp  18545  smndex1mnd  18547  smndex1id  18548  grp1  18680  grp1inv  18681  mulgfval  18700  triv1nsgd  18799  1nsgtrivd  18800  symg2bas  18998  symgvalstruct  19002  symgvalstructOLD  19003  idrespermg  19017  pmtrsn  19125  psgnsn  19126  abl1  19465  gsum2d2  19573  gsumcom2  19574  dprdz  19631  dprdsn  19637  dprd2da  19643  simpgnsgd  19701  2nsgsimpgd  19703  ring1  19839  pwssplit3  20321  rng1nnzr  20543  frlmip  20983  islindf4  21043  evlssca  21297  mpfind  21315  evls1sca  21487  pf1ind  21519  mattposvs  21602  mat1dimelbas  21618  mat1dimscm  21622  mat1dimmul  21623  mat1rhmval  21626  m1detdiag  21744  mdetrlin  21749  mdetrsca2  21751  mdetrlin2  21754  mdetunilem5  21763  smadiadetglem2  21819  basdif0  22101  ordtbas  22341  leordtval2  22361  dishaus  22531  discmp  22547  conncompid  22580  dis2ndc  22609  dislly  22646  dis1stc  22648  unisngl  22676  1stckgen  22703  ptbasfi  22730  dfac14lem  22766  dfac14  22767  ptrescn  22788  xkoptsub  22803  pt1hmeo  22955  xpstopnlem1  22958  ptcmpfi  22962  isufil2  23057  ufileu  23068  filufint  23069  uffix  23070  uffixsn  23074  flimclslem  23133  ptcmplem1  23201  cnextfval  23211  imasdsf1olem  23524  icccmplem1  23983  icccmplem2  23984  rrxip  24552  rrxsca  24558  ehl1eudis  24582  elply2  25355  plyss  25358  plyeq0lem  25369  taylfval  25516  axlowdimlem15  27322  axlowdim  27327  snstriedgval  27406  vtxvalsnop  27409  iedgvalsnop  27410  upgr1eop  27483  upgr1eopALT  27485  uspgr1eop  27612  usgr1eop  27615  lfuhgr1v0e  27619  1loopgrvd2  27868  1loopgrvd0  27869  p1evtxdeqlem  27877  p1evtxdeq  27878  p1evtxdp1  27879  uspgrloopvtx  27880  uspgrloopiedg  27882  uspgrloopedg  27883  wlkp1lem4  28041  0pthonv  28489  eupth2lem3  28596  wlkl0  28727  0ofval  29145  suppovss  31013  resf1o  31061  gsumpart  31311  zar0ring  31824  ordtconnlem1  31870  esumpr  32030  esumrnmpt2  32032  esumfzf  32033  esum2dlem  32056  esum2d  32057  esumiun  32058  prsiga  32095  rossros  32144  cntnevol  32192  carsgclctunlem1  32280  omsmeas  32286  eulerpartlemgs2  32343  ccatmulgnn0dir  32517  ofcs1  32519  actfunsnf1o  32580  actfunsnrndisj  32581  reprsuc  32591  breprexplema  32606  bnj918  32742  bnj95  32840  bnj1452  33028  bnj1489  33032  fineqvac  33062  subfacp1lem5  33142  erdszelem5  33153  erdszelem8  33156  cvmliftlem4  33246  cvmliftlem5  33247  cvmlift2lem6  33266  cvmlift2lem9  33269  cvmlift2lem12  33272  satfv1lem  33320  prv1n  33389  sexp2  33789  sexp3  33795  naddcllem  33827  conway  33989  etasslt  34003  slerec  34009  0slt1s  34019  ssltleft  34050  ssltright  34051  cofcutr  34088  addsval  34122  fobigcup  34198  elsingles  34216  fnsingle  34217  fvsingle  34218  dfiota3  34221  brapply  34236  brsuccf  34239  funpartlem  34240  altopthsn  34259  altxpsspw  34275  hfsn  34477  neibastop2lem  34545  topjoin  34550  onpsstopbas  34615  bj-snsetex  35149  bj-elsngl  35154  bj-2uplex  35208  bj-restsn  35249  f1omptsnlem  35503  mptsnunlem  35505  topdifinffinlem  35514  finixpnum  35758  ptrest  35772  poimirlem3  35776  poimirlem4  35777  poimirlem28  35801  fdc  35899  heiborlem3  35967  heiborlem8  35972  ismrer1  35992  grposnOLD  36036  zrdivrng  36107  ecexALTV  36462  eccnvepex  36466  ldualset  37135  lineset  37748  ispointN  37752  dvaset  39015  dvhset  39091  dibval  39152  dibfna  39164  sticksstones9  40107  frlmsnic  40260  evlsbagval  40272  elrfi  40513  mzpincl  40553  mzpcompact2lem  40570  wopprc  40849  dfac11  40884  kelac2  40887  pwslnmlem1  40914  pwslnm  40916  sn1dom  41112  pr2dom  41113  tr3dom  41114  fvilbdRP  41268  brtrclfv2  41305  frege110  41551  frege133  41574  k0004lem3  41729  mnuprdlem1  41860  mnuprdlem2  41861  snelpwrVD  42421  fnchoice  42542  mpct  42711  elmapsnd  42714  difmapsn  42722  unirnmapsn  42724  ssmapsn  42726  limcresiooub  43154  limcresioolb  43155  cnfdmsn  43394  dvsinax  43425  fourierdlem48  43666  fourierdlem49  43667  salexct3  43852  salgencntex  43853  salgensscntex  43854  sge0sn  43888  sge0p1  43923  sge0xp  43938  ovnovollem1  44165  ovnovollem2  44166  vonvolmbllem  44169  fsetsnf  44513  fsetsnf1  44514  fsetsnfo  44515  cfsetsnfsetfo  44522  setsv  44799  nnsum3primesprm  45211  mpoexxg2  45642  mapsnop  45649  lindsrng01  45778  snlindsntorlem  45780  snlindsntor  45781  lmod1lem1  45797  lmod1lem2  45798  lmod1lem3  45799  lmod1lem4  45800  lmod1lem5  45801  lmod1  45802  lmod1zr  45803  fv1arycl  45952  1arympt1fv  45954  1arymaptfo  45958  eufsn2  46139  prstchomval  46324  mndtcbasval  46336  mndtchom  46340  mndtcco  46341  aacllem  46474