Theorem snex 5451

Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5401. (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 5450	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
2		snprc 4742	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
3	2	biimpi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴} = ∅)
4		0ex 5325	. . 3 ⊢ ∅ ∈ V
5	3, 4	eqeltrdi 2852	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
6	1, 5	pm2.61i 182	1 ⊢ {𝐴} ∈ V

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-pr 4651

This theorem is referenced by:  prex  5452  snelpwiOLD  5464  intidOLD  5478  elopg  5486  opi1  5488  op1stb  5491  opnz  5493  opeqsng  5522  opeqpr  5524  snopeqop  5525  opthwiener  5533  uniop  5534  0sn0ep  5603  frirr  5676  opthprc  5764  frsn  5787  relop  5875  snsn0non  6520  onnev  6522  funsneqopb  7186  fsnex  7319  tpex  7781  difsnexi  7796  sucexb  7840  elxp4  7962  elxp5  7963  fvclex  7999  1stval  8032  2ndval  8033  fnse  8174  suppsnop  8219  brtpos2  8273  frrlem13  8339  wfrlem15OLD  8379  tfrlem12  8445  tfrlem16  8449  1oex  8532  naddunif  8749  mapsnd  8944  fvdiagfn  8949  mapsnconst  8950  mapsncnv  8951  mapsnf1o2  8952  ralxpmap  8954  elixpsn  8995  ixpsnf1o  8996  mapsnf1o  8997  ensn1  9082  ensn1OLD  9083  en1bOLD  9089  2dom  9095  mapsnend  9101  snmapen  9103  en2sn  9106  en2snOLD  9107  xpsnen  9121  endisj  9124  xpsnen2g  9131  domunsncan  9138  enfixsn  9147  disjenex  9201  domssex2  9203  domssex  9204  map2xp  9213  pssnn  9234  phplem2OLD  9281  snnen2o  9300  isinf  9323  isinfOLD  9324  ac6sfi  9348  xpfiOLD  9387  fodomfiOLD  9398  pwfilemOLD  9416  fczfsuppd  9455  snopfsupp  9460  fisn  9496  tc2  9811  tcsni  9812  ranksuc  9934  djuex  9977  fseqenlem1  10093  djuassen  10248  mapdjuen  10250  djudom1  10252  djuinf  10258  ackbij1lem5  10292  cfsuc  10326  dcomex  10516  axdc3lem4  10522  axdc4lem  10524  ttukeylem3  10580  brdom7disj  10600  brdom6disj  10601  fpwwe2lem12  10711  nn0ex  12559  hashxplem  14482  hashf1lem1  14504  hashge3el3dif  14536  ofs1  15019  climconst2  15594  ramub1lem2  17074  cshwsex  17148  setsvalg  17213  setsid  17255  pwsbas  17547  pwsle  17552  pwssca  17556  pwssnf1o  17558  imasplusg  17577  imasmulr  17578  imasvsca  17580  imasip  17581  acsfn  17717  homaval  18098  funcsetcestrclem1  18223  mgm1  18696  sgrp1  18767  mnd1  18814  mnd1id  18815  efmnd1bas  18928  idresefmnd  18934  smndex1bas  18941  smndex1sgrp  18943  smndex1mnd  18945  smndex1id  18946  grp1  19087  grp1inv  19088  mulgfval  19109  triv1nsgd  19213  1nsgtrivd  19214  symg2bas  19434  symgvalstructOLD  19439  idrespermg  19453  pmtrsn  19561  psgnsn  19562  abl1  19908  dprdz  20074  dprdsn  20080  simpgnsgd  20144  2nsgsimpgd  20146  ring1  20333  rng1nnzr  20798  pwssplit3  21083  cnfldex  21390  pzriprnglem13  21527  pzriprnglem14  21528  frlmip  21821  islindf4  21881  evlssca  22136  psdmul  22193  evls1sca  22348  mattposvs  22482  mat1dimelbas  22498  mat1dimscm  22502  mat1dimmul  22503  mat1rhmval  22506  m1detdiag  22624  mdetrlin  22629  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  smadiadetglem2  22699  basdif0  22981  ordtbas  23221  leordtval2  23241  conncompid  23460  ptbasfi  23610  dfac14lem  23646  dfac14  23647  ptrescn  23668  xkoptsub  23683  pt1hmeo  23835  xpstopnlem1  23838  ufileu  23948  filufint  23949  uffix  23950  uffixsn  23954  flimclslem  24013  ptcmplem1  24081  imasdsf1olem  24404  icccmplem1  24863  icccmplem2  24864  rrxip  25443  rrxsca  25449  ehl1eudis  25473  elply2  26255  plyss  26258  plyeq0lem  26269  taylfval  26418  ssltsn  27855  slerec  27882  0slt1s  27892  ssltleft  27927  ssltright  27928  addsval  28013  addsuniflem  28052  negsid  28091  negsunif  28105  mulsval  28153  ssltmul1  28191  ssltmul2  28192  precsexlem1  28249  precsexlem2  28250  precsexlem11  28259  nohalf  28425  0reno  28447  axlowdimlem15  28989  axlowdim  28994  snstriedgval  29073  vtxvalsnop  29076  iedgvalsnop  29077  upgr1eop  29150  upgr1eopALT  29152  uspgr1eop  29282  usgr1eop  29285  1loopgrvd2  29539  1loopgrvd0  29540  p1evtxdeqlem  29548  p1evtxdeq  29549  p1evtxdp1  29550  uspgrloopvtx  29551  uspgrloopiedg  29553  uspgrloopedg  29554  wlkp1lem4  29712  0pthonv  30161  eupth2lem3  30268  wlkl0  30399  0ofval  30819  suppovss  32697  resf1o  32744  elrspunsn  33422  drngidlhash  33427  zar0ring  33824  ordtconnlem1  33870  esumpr  34030  esumrnmpt2  34032  esumfzf  34033  prsiga  34095  rossros  34144  cntnevol  34192  omsmeas  34288  ccatmulgnn0dir  34519  ofcs1  34521  actfunsnf1o  34581  actfunsnrndisj  34582  reprsuc  34592  breprexplema  34607  bnj918  34742  bnj95  34840  bnj1489  35032  fineqvac  35073  subfacp1lem5  35152  erdszelem5  35163  erdszelem8  35166  cvmliftlem4  35256  cvmliftlem5  35257  cvmlift2lem6  35276  cvmlift2lem9  35279  cvmlift2lem12  35282  satfv1lem  35330  prv1n  35399  brapply  35902  brsuccf  35905  altopthsn  35925  hfsn  36143  neibastop2lem  36326  topjoin  36331  onpsstopbas  36396  weiunse  36434  bj-2uplex  36988  bj-restsn  37048  finixpnum  37565  ptrest  37579  poimirlem3  37583  poimirlem4  37584  poimirlem28  37608  fdc  37705  heiborlem8  37778  ismrer1  37798  grposnOLD  37842  zrdivrng  37913  ecexALTV  38287  eccnvepex  38291  ldualset  39081  lineset  39695  dvaset  40962  dvhset  41038  dibval  41099  dibfna  41111  sticksstones9  42111  frlmsnic  42495  evlsvvval  42518  evlsevl  42526  elrfi  42650  wopprc  42987  dfac11  43019  kelac2  43022  safesnsupfidom1o  43379  sn1dom  43488  pr2dom  43489  tr3dom  43490  fvilbdRP  43652  brtrclfv2  43689  frege110  43935  frege133  43958  k0004lem3  44111  mnuprdlem1  44241  mnuprdlem2  44242  snelpwrVD  44802  fnchoice  44929  elmapsnd  45111  difmapsn  45119  unirnmapsn  45121  ssmapsn  45123  limcresiooub  45563  limcresioolb  45564  cnfdmsn  45803  dvsinax  45834  fourierdlem48  46075  fourierdlem49  46076  sge0sn  46300  sge0p1  46335  ovnovollem1  46577  ovnovollem2  46578  vonvolmbllem  46581  fsetsnf  46966  fsetsnf1  46967  fsetsnfo  46968  cfsetsnfsetfo  46975  setsv  47252  nnsum3primesprm  47664  mapsnop  48069  lindsrng01  48197  snlindsntorlem  48199  snlindsntor  48200  lmod1lem1  48216  lmod1lem2  48217  lmod1lem3  48218  lmod1lem4  48219  lmod1lem5  48220  lmod1  48221  lmod1zr  48222  fv1arycl  48371  1arympt1fv  48373  1arymaptfo  48377  eufsn2  48556  prstchomval  48741  mndtcbasval  48753  mndtchom  48757  mndtcco  48758  aacllem  48895