Theorem snex 5369

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5316. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.)

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		snexg 5368	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
2		snprc 4665	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
3	2	biimpi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
4		0ex 5240	. . 3 ⊢ ∅ ∈ V
5	3, 4	eqeltrdi 2839	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
6	1, 5	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4278  {csn 4571

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4279  df-sn 4572  df-pr 4574

This theorem is referenced by:  prex  5370  elopg  5401  opi1  5403  op1stb  5406  opnz  5408  opeqsng  5438  opeqpr  5440  snopeqop  5441  opthwiener  5449  uniop  5450  0sn0ep  5515  frirr  5587  opthprc  5675  frsn  5699  relop  5785  snsn0non  6427  onnev  6429  funsneqopb  7080  fsnex  7212  tpex  7674  difsnexi  7689  sucexb  7732  elxp4  7847  elxp5  7848  fvclex  7886  1stval  7918  2ndval  7919  fnse  8058  suppsnop  8103  brtpos2  8157  frrlem13  8223  tfrlem12  8303  tfrlem16  8307  1oex  8390  naddunif  8603  mapsnd  8805  fvdiagfn  8810  mapsnconst  8811  mapsncnv  8812  mapsnf1o2  8813  ralxpmap  8815  elixpsn  8856  ixpsnf1o  8857  mapsnf1o  8858  ensn1  8938  2dom  8947  mapsnend  8953  snmapen  8955  en2sn  8958  xpsnen  8969  endisj  8972  xpsnen2g  8978  domunsncan  8985  enfixsn  8994  disjenex  9043  domssex2  9045  domssex  9046  map2xp  9055  pssnn  9073  snnen2o  9124  isinf  9144  ac6sfi  9163  fodomfiOLD  9209  fczfsuppd  9265  snopfsupp  9270  fisn  9306  tc2  9625  tcsni  9626  ranksuc  9753  djuex  9796  fseqenlem1  9910  djuassen  10065  mapdjuen  10067  djudom1  10069  djuinf  10075  ackbij1lem5  10109  cfsuc  10143  dcomex  10333  axdc3lem4  10339  axdc4lem  10341  ttukeylem3  10397  brdom7disj  10417  brdom6disj  10418  fpwwe2lem12  10528  nn0ex  12382  hashxplem  14335  hashf1lem1  14357  hashge3el3dif  14389  ofs1  14872  climconst2  15450  ramub1lem2  16934  cshwsex  17007  setsvalg  17072  setsid  17113  pwsbas  17386  pwsle  17391  pwssca  17395  pwssnf1o  17397  imasplusg  17416  imasmulr  17417  imasvsca  17419  imasip  17420  acsfn  17560  homaval  17933  funcsetcestrclem1  18055  mgm1  18561  sgrp1  18632  mnd1  18682  mnd1id  18683  efmnd1bas  18796  idresefmnd  18802  smndex1bas  18809  smndex1sgrp  18811  smndex1mnd  18813  smndex1id  18814  grp1  18955  grp1inv  18956  mulgfval  18977  triv1nsgd  19080  1nsgtrivd  19081  symg2bas  19300  idrespermg  19318  pmtrsn  19426  psgnsn  19427  abl1  19773  dprdz  19939  dprdsn  19945  simpgnsgd  20009  2nsgsimpgd  20011  ring1  20223  rng1nnzr  20685  pwssplit3  20990  cnfldex  21289  pzriprnglem13  21425  pzriprnglem14  21426  frlmip  21710  islindf4  21770  evlssca  22019  psdmul  22076  evls1sca  22233  mattposvs  22365  mat1dimelbas  22381  mat1dimscm  22385  mat1dimmul  22386  mat1rhmval  22389  m1detdiag  22507  mdetrlin  22512  mdetrsca2  22514  mdetrlin2  22517  mdetunilem5  22526  smadiadetglem2  22582  basdif0  22863  ordtbas  23102  leordtval2  23122  conncompid  23341  ptbasfi  23491  dfac14lem  23527  dfac14  23528  ptrescn  23549  xkoptsub  23564  pt1hmeo  23716  xpstopnlem1  23719  ufileu  23829  filufint  23830  uffix  23831  uffixsn  23835  flimclslem  23894  ptcmplem1  23962  imasdsf1olem  24283  icccmplem1  24733  icccmplem2  24734  rrxip  25312  rrxsca  25318  ehl1eudis  25342  elply2  26123  plyss  26126  plyeq0lem  26137  taylfval  26288  ssltsnb  27727  slerec  27755  eqscut3  27760  0slt1s  27768  ssltleft  27810  ssltright  27811  addsval  27900  addsuniflem  27939  negsid  27978  negsunif  27992  mulsval  28043  ssltmul1  28081  ssltmul2  28082  precsexlem1  28140  precsexlem2  28141  precsexlem11  28150  n0sfincut  28277  0reno  28394  axlowdimlem15  28929  axlowdim  28934  snstriedgval  29011  vtxvalsnop  29014  iedgvalsnop  29015  upgr1eop  29088  upgr1eopALT  29090  uspgr1eop  29220  usgr1eop  29223  1loopgrvd2  29477  1loopgrvd0  29478  p1evtxdeqlem  29486  p1evtxdeq  29487  p1evtxdp1  29488  uspgrloopvtx  29489  uspgrloopiedg  29491  uspgrloopedg  29492  wlkp1lem4  29648  0pthonv  30101  eupth2lem3  30208  wlkl0  30339  0ofval  30759  suppovss  32654  resf1o  32705  elrgspnlem4  33204  elrspunsn  33386  drngidlhash  33391  zar0ring  33883  ordtconnlem1  33929  esumpr  34071  esumrnmpt2  34073  esumfzf  34074  prsiga  34136  rossros  34185  cntnevol  34233  omsmeas  34328  ccatmulgnn0dir  34547  ofcs1  34549  actfunsnf1o  34609  actfunsnrndisj  34610  reprsuc  34620  breprexplema  34635  bnj918  34770  bnj95  34868  bnj1489  35060  fineqvac  35131  subfacp1lem5  35220  erdszelem5  35231  erdszelem8  35234  cvmliftlem4  35324  cvmliftlem5  35325  cvmlift2lem6  35344  cvmlift2lem9  35347  cvmlift2lem12  35350  satfv1lem  35398  prv1n  35467  brapply  35972  brsuccf  35975  altopthsn  35995  hfsn  36213  neibastop2lem  36394  topjoin  36399  onpsstopbas  36464  weiunse  36502  bj-2uplex  37056  bj-restsn  37116  finixpnum  37645  ptrest  37659  poimirlem3  37663  poimirlem4  37664  poimirlem28  37688  fdc  37785  heiborlem8  37858  ismrer1  37878  grposnOLD  37922  zrdivrng  37993  ldualset  39164  lineset  39777  dvaset  41044  dvhset  41120  dibval  41181  dibfna  41193  sticksstones9  42187  frlmsnic  42573  evlsvvval  42596  evlsevl  42604  elrfi  42727  wopprc  43063  dfac11  43095  kelac2  43098  safesnsupfidom1o  43450  sn1dom  43559  pr2dom  43560  tr3dom  43561  fvilbdRP  43723  brtrclfv2  43760  frege110  44006  frege133  44029  k0004lem3  44182  mnuprdlem1  44305  mnuprdlem2  44306  snelpwrVD  44863  nregmodelf1o  45048  fnchoice  45066  elmapsnd  45241  difmapsn  45249  unirnmapsn  45251  ssmapsn  45253  limcresiooub  45680  limcresioolb  45681  cnfdmsn  45920  dvsinax  45951  fourierdlem48  46192  fourierdlem49  46193  sge0sn  46417  sge0p1  46452  ovnovollem1  46694  ovnovollem2  46695  vonvolmbllem  46698  fsetsnf  47082  fsetsnf1  47083  fsetsnfo  47084  cfsetsnfsetfo  47091  setsv  47409  nnsum3primesprm  47821  mapsnop  48375  lindsrng01  48500  snlindsntorlem  48502  snlindsntor  48503  lmod1lem1  48519  lmod1lem2  48520  lmod1lem3  48521  lmod1lem4  48522  lmod1lem5  48523  lmod1  48524  lmod1zr  48525  fv1arycl  48669  1arympt1fv  48671  1arymaptfo  48675  eufsn2  48874  discsubclem  49095  discsubc  49096  iinfconstbas  49098  diag1f1lem  49338  setcsnterm  49522  setc1ocofval  49526  isinito2lem  49530  idfudiag1  49557  diag1f1olem  49565  prstchomval  49591  mndtcbasval  49612  mndtchom  49616  mndtcco  49617  incat  49633  setc1onsubc  49634  aacllem  49833