MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snex Structured version   Visualization version   GIF version

Theorem snex 4938
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4882. (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.
StepHypRef Expression
1 dfsn2 4223 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4302 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 678 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2715 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 4937 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3297 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2734 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4285 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 206 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4823 . . 3 ∅ ∈ V
119, 10syl6eqel 2738 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 176 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1523  wcel 2030  Vcvv 3231  c0 3948  {csn 4210  {cpr 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-nul 3949  df-sn 4211  df-pr 4213
This theorem is referenced by:  prex  4939  elALT  4940  dtruALT2  4941  snelpwi  4942  snelpw  4943  rext  4946  sspwb  4947  intid  4956  moabex  4957  nnullss  4960  exss  4961  elopg  4964  opi1  4966  op1stb  4969  opnz  4971  opeqsn  4996  opeqpr  4997  propssopi  5000  opthwiener  5005  uniop  5006  frirr  5120  frsn  5223  xpsspw  5266  relop  5305  onnev  5886  funopg  5960  funsneqopsn  6457  funsneqop  6458  fsnex  6578  tpex  6999  snnex  7008  snnexOLD  7009  difsnexi  7012  sucexb  7051  soex  7151  elxp4  7152  elxp5  7153  opabex3d  7187  opabex3  7188  1stval  7212  2ndval  7213  fo1st  7230  fo2nd  7231  mpt2exxg  7289  cnvf1o  7321  fnse  7339  suppsnop  7354  brtpos2  7403  wfrlem15  7474  tfrlem12  7530  tfrlem16  7534  mapsn  7941  fvdiagfn  7944  mapsnconst  7945  mapsncnv  7946  mapsnf1o2  7947  ralxpmap  7949  elixpsn  7989  ixpsnf1o  7990  mapsnf1o  7991  ensn1  8061  en1b  8065  mapsnen  8076  xpsnen  8085  endisj  8088  xpsnen2g  8094  domunsncan  8101  enfixsn  8110  domunsn  8151  fodomr  8152  disjenex  8159  domssex2  8161  domssex  8162  map2xp  8171  phplem2  8181  isinf  8214  pssnn  8219  findcard2  8241  ac6sfi  8245  xpfi  8272  fodomfi  8280  pwfilem  8301  fczfsuppd  8334  snopfsupp  8339  fisn  8374  marypha1lem  8380  brwdom2  8519  unxpwdom2  8534  elirrv  8542  epfrs  8645  tc2  8656  tcsni  8657  ranksuc  8766  fseqenlem1  8885  dfac5lem2  8985  dfac5lem3  8986  dfac5lem4  8987  kmlem2  9011  cdafn  9029  cdaval  9030  cdaassen  9042  mapcdaen  9044  cdadom1  9046  cdainf  9052  ackbij1lem5  9084  cfsuc  9117  isfin1-3  9246  hsmexlem4  9289  axcc2lem  9296  dcomex  9307  axdc3lem4  9313  axdc4lem  9315  ttukeylem3  9371  brdom7disj  9391  brdom6disj  9392  fpwwe2lem13  9502  canthwe  9511  canthp1lem1  9512  uniwun  9600  rankcf  9637  nn0ex  11336  hashxplem  13258  hashmap  13260  hashbclem  13274  hashf1lem1  13277  hashge3el3dif  13306  ofs1  13755  climconst2  14323  incexclem  14612  ramub1lem2  15778  cshwsex  15854  setsvalg  15934  setsid  15961  pwsbas  16194  pwsle  16199  pwssca  16203  pwssnf1o  16205  imasplusg  16224  imasmulr  16225  imasvsca  16227  imasip  16228  xpsc  16264  acsfn  16367  isfunc  16571  homaf  16727  homaval  16728  funcsetcestrclem1  16841  mgm1  17304  sgrp1  17340  mnd1  17378  mnd1id  17379  grp1  17569  grp1inv  17570  symg2bas  17864  idrespermg  17877  pmtrsn  17985  psgnsn  17986  abl1  18315  gsum2d2  18419  gsumcom2  18420  dprdz  18475  dprdsn  18481  dprd2da  18487  ring1  18648  pwssplit3  19109  drngnidl  19277  drnglpir  19301  rng1nnzr  19322  evlssca  19570  mpfind  19584  evls1sca  19736  pf1ind  19767  frlmip  20165  islindf4  20225  mattposvs  20309  mat1dimelbas  20325  mat1dimscm  20329  mat1dimmul  20330  mat1rhmval  20333  m1detdiag  20451  mdetrlin  20456  mdetrsca2  20458  mdetrlin2  20461  mdetunilem5  20470  smadiadetglem2  20526  basdif0  20805  ordtbas  21044  leordtval2  21064  dishaus  21234  discmp  21249  conncompid  21282  dis2ndc  21311  dislly  21348  dis1stc  21350  unisngl  21378  1stckgen  21405  ptbasfi  21432  dfac14lem  21468  dfac14  21469  ptrescn  21490  xkoptsub  21505  pt1hmeo  21657  xpstopnlem1  21660  ptcmpfi  21664  isufil2  21759  ufileu  21770  filufint  21771  uffix  21772  uffixsn  21776  flimclslem  21835  ptcmplem1  21903  cnextfval  21913  imasdsf1olem  22225  icccmplem1  22672  icccmplem2  22673  rrxip  23224  elply2  23997  plyss  24000  plyeq0lem  24011  taylfval  24158  axlowdimlem15  25881  axlowdim  25886  snstriedgval  25975  vtxvalsnop  25978  iedgvalsnop  25979  upgr1eop  26055  upgr1eopALT  26057  uspgr1eop  26184  usgr1eop  26187  lfuhgr1v0e  26191  1loopgrvd2  26455  1loopgrvd0  26456  p1evtxdeqlem  26464  p1evtxdeq  26465  p1evtxdp1  26466  uspgrloopvtx  26467  uspgrloopiedg  26469  uspgrloopedg  26470  wlkp1lem4  26629  0pthonv  27107  eupth2lem3  27214  0ofval  27770  resf1o  29633  ordtconnlem1  30098  esumpr  30256  esumrnmpt2  30258  esumfzf  30259  esum2dlem  30282  esum2d  30283  esumiun  30284  prsiga  30322  rossros  30371  cntnevol  30419  carsgclctunlem1  30507  omsmeas  30513  eulerpartlemgs2  30570  ccatmulgnn0dir  30747  ofcs1  30749  actfunsnf1o  30810  actfunsnrndisj  30811  reprsuc  30821  breprexplema  30836  bnj918  30962  bnj95  31060  bnj1452  31246  bnj1489  31250  subfacp1lem5  31292  erdszelem5  31303  erdszelem8  31306  cvmliftlem4  31396  cvmliftlem5  31397  cvmlift2lem6  31416  cvmlift2lem9  31419  cvmlift2lem12  31422  conway  32035  etasslt  32045  slerec  32048  fobigcup  32132  elsingles  32150  fnsingle  32151  fvsingle  32152  dfiota3  32155  brapply  32170  brsuccf  32173  funpartlem  32174  altopthsn  32193  altxpsspw  32209  hfsn  32411  neibastop2lem  32480  topjoin  32485  onpsstopbas  32554  bj-sels  33075  bj-snsetex  33076  bj-elsngl  33081  bj-2uplex  33135  bj-restsn  33160  bj-snmoore  33193  f1omptsnlem  33313  mptsnunlem  33315  topdifinffinlem  33325  finixpnum  33524  ptrest  33538  poimirlem3  33542  poimirlem4  33543  poimirlem28  33567  fdc  33671  heiborlem3  33742  heiborlem8  33747  ismrer1  33767  grposnOLD  33811  zrdivrng  33882  ldualset  34730  lineset  35342  ispointN  35346  dvaset  36610  dvhset  36687  dibval  36748  dibfna  36760  elrfi  37574  mzpincl  37614  mzpcompact2lem  37631  wopprc  37914  dfac11  37949  kelac2  37952  pwslnmlem1  37979  pwslnm  37981  fvilbdRP  38299  brtrclfv2  38336  frege110  38584  frege133  38607  k0004lem3  38764  snelpwrVD  39380  fnchoice  39502  mapsnd  39702  mapsnend  39705  mpct  39707  elmapsnd  39710  difmapsn  39718  unirnmapsn  39720  ssmapsn  39722  limcresiooub  40192  limcresioolb  40193  cnfdmsn  40413  dvsinax  40445  fourierdlem48  40689  fourierdlem49  40690  salexct3  40878  salgencntex  40879  salgensscntex  40880  sge0sn  40914  sge0p1  40949  sge0xp  40964  ovnovollem1  41191  ovnovollem2  41192  vonvolmbllem  41195  setsv  41673  nnsum3primesprm  42003  mpt2exxg2  42441  mapsnop  42448  lindsrng01  42582  snlindsntorlem  42584  snlindsntor  42585  lmod1lem1  42601  lmod1lem2  42602  lmod1lem3  42603  lmod1lem4  42604  lmod1lem5  42605  lmod1  42606  lmod1zr  42607  aacllem  42875
  Copyright terms: Public domain W3C validator