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

Theorem snex 5098
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5052. (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 4383 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4461 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 558 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2870 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 5097 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3459 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2889 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4444 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 207 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4984 . . 3 ∅ ∈ V
119, 10syl6eqel 2893 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 176 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1637  wcel 2156  Vcvv 3391  c0 4116  {csn 4370  {cpr 4372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-un 3774  df-nul 4117  df-sn 4371  df-pr 4373
This theorem is referenced by:  prex  5099  elALT  5100  dtruALT2  5101  snelpwi  5102  snelpw  5103  rext  5106  sspwb  5107  intid  5116  moabex  5117  nnullss  5120  exss  5121  elopg  5124  opi1  5126  op1stb  5129  opnz  5131  opeqsng  5156  opeqsnOLD  5158  opeqpr  5159  snopeqop  5160  opthwiener  5169  uniop  5170  0sn0ep  5228  frirr  5288  frsn  5391  xpsspw  5434  relop  5474  onnev  6057  funopg  6131  funsneqopsnOLD  6637  funsneqopOLD  6638  funsneqopb  6639  fsnex  6758  tpex  7183  snnex  7192  snnexOLD  7193  difsnexi  7196  sucexb  7235  soex  7335  elxp4  7336  elxp5  7337  opabex3d  7371  opabex3  7372  1stval  7396  2ndval  7397  fo1st  7414  fo2nd  7415  mpt2exxg  7473  cnvf1o  7506  fnse  7524  suppsnop  7539  brtpos2  7589  wfrlem15  7661  tfrlem12  7717  tfrlem16  7721  mapsnd  8130  fvdiagfn  8135  mapsnconst  8136  mapsncnv  8137  mapsnf1o2  8138  ralxpmap  8140  elixpsn  8180  ixpsnf1o  8181  mapsnf1o  8182  ensn1  8252  en1b  8256  mapsnend  8267  snmapen  8269  xpsnen  8279  endisj  8282  xpsnen2g  8288  domunsncan  8295  enfixsn  8304  domunsn  8345  fodomr  8346  disjenex  8353  domssex2  8355  domssex  8356  map2xp  8365  phplem2  8375  isinf  8408  pssnn  8413  findcard2  8435  ac6sfi  8439  xpfi  8466  fodomfi  8474  pwfilem  8495  fczfsuppd  8528  snopfsupp  8533  fisn  8568  marypha1lem  8574  brwdom2  8713  unxpwdom2  8728  elirrv  8736  epfrs  8850  tc2  8861  tcsni  8862  ranksuc  8971  djuex  9014  fseqenlem1  9126  dfac5lem2  9226  dfac5lem3  9227  dfac5lem4  9228  kmlem2  9254  cdafn  9272  cdaval  9273  cdaassen  9285  mapcdaen  9287  cdadom1  9289  cdainf  9295  ackbij1lem5  9327  cfsuc  9360  isfin1-3  9489  hsmexlem4  9532  axcc2lem  9539  dcomex  9550  axdc3lem4  9556  axdc4lem  9558  ttukeylem3  9614  brdom7disj  9634  brdom6disj  9635  fpwwe2lem13  9745  canthwe  9754  canthp1lem1  9755  uniwun  9843  rankcf  9880  nn0ex  11561  hashxplem  13433  hashmap  13435  hashbclem  13449  hashf1lem1  13452  hashge3el3dif  13481  ofs1  13930  climconst2  14498  incexclem  14786  ramub1lem2  15944  cshwsex  16015  setsvalg  16094  setsid  16121  pwsbas  16348  pwsle  16353  pwssca  16357  pwssnf1o  16359  imasplusg  16378  imasmulr  16379  imasvsca  16381  imasip  16382  xpsc  16418  acsfn  16520  isfunc  16724  homaf  16880  homaval  16881  funcsetcestrclem1  16995  mgm1  17458  sgrp1  17494  mnd1  17532  mnd1id  17533  grp1  17723  grp1inv  17724  symg2bas  18015  idrespermg  18028  pmtrsn  18136  psgnsn  18137  abl1  18466  gsum2d2  18570  gsumcom2  18571  dprdz  18627  dprdsn  18633  dprd2da  18639  ring1  18800  pwssplit3  19264  drngnidl  19434  drnglpir  19458  rng1nnzr  19479  evlssca  19726  mpfind  19740  evls1sca  19892  pf1ind  19923  frlmip  20324  islindf4  20384  mattposvs  20469  mat1dimelbas  20485  mat1dimscm  20489  mat1dimmul  20490  mat1rhmval  20493  m1detdiag  20611  mdetrlin  20616  mdetrsca2  20618  mdetrlin2  20621  mdetunilem5  20630  smadiadetglem2  20687  basdif0  20968  ordtbas  21207  leordtval2  21227  dishaus  21397  discmp  21412  conncompid  21445  dis2ndc  21474  dislly  21511  dis1stc  21513  unisngl  21541  1stckgen  21568  ptbasfi  21595  dfac14lem  21631  dfac14  21632  ptrescn  21653  xkoptsub  21668  pt1hmeo  21820  xpstopnlem1  21823  ptcmpfi  21827  isufil2  21922  ufileu  21933  filufint  21934  uffix  21935  uffixsn  21939  flimclslem  21998  ptcmplem1  22066  cnextfval  22076  imasdsf1olem  22388  icccmplem1  22835  icccmplem2  22836  rrxip  23389  elply2  24165  plyss  24168  plyeq0lem  24179  taylfval  24326  axlowdimlem15  26049  axlowdim  26054  snstriedgval  26143  vtxvalsnop  26146  iedgvalsnop  26147  upgr1eop  26223  upgr1eopALT  26225  uspgr1eop  26354  usgr1eop  26357  lfuhgr1v0e  26361  1loopgrvd2  26626  1loopgrvd0  26627  p1evtxdeqlem  26635  p1evtxdeq  26636  p1evtxdp1  26637  uspgrloopvtx  26638  uspgrloopiedg  26640  uspgrloopedg  26641  wlkp1lem4  26800  0pthonv  27301  eupth2lem3  27408  wlkl0  27546  0ofval  27969  resf1o  29831  ordtconnlem1  30294  esumpr  30452  esumrnmpt2  30454  esumfzf  30455  esum2dlem  30478  esum2d  30479  esumiun  30480  prsiga  30518  rossros  30567  cntnevol  30615  carsgclctunlem1  30703  omsmeas  30709  eulerpartlemgs2  30766  ccatmulgnn0dir  30943  ofcs1  30945  actfunsnf1o  31006  actfunsnrndisj  31007  reprsuc  31017  breprexplema  31032  bnj918  31157  bnj95  31255  bnj1452  31441  bnj1489  31445  subfacp1lem5  31487  erdszelem5  31498  erdszelem8  31501  cvmliftlem4  31591  cvmliftlem5  31592  cvmlift2lem6  31611  cvmlift2lem9  31614  cvmlift2lem12  31617  conway  32229  etasslt  32239  slerec  32242  fobigcup  32326  elsingles  32344  fnsingle  32345  fvsingle  32346  dfiota3  32349  brapply  32364  brsuccf  32367  funpartlem  32368  altopthsn  32387  altxpsspw  32403  hfsn  32605  neibastop2lem  32674  topjoin  32679  onpsstopbas  32744  bj-sels  33258  bj-snsetex  33259  bj-elsngl  33264  bj-2uplex  33318  bj-restsn  33344  bj-snmoore  33377  f1omptsnlem  33498  mptsnunlem  33500  topdifinffinlem  33509  cnfin0  33554  cnfinltrel  33555  finixpnum  33705  ptrest  33719  poimirlem3  33723  poimirlem4  33724  poimirlem28  33748  fdc  33850  heiborlem3  33921  heiborlem8  33926  ismrer1  33946  grposnOLD  33990  zrdivrng  34061  ldualset  34903  lineset  35516  ispointN  35520  dvaset  36783  dvhset  36859  dibval  36920  dibfna  36932  elrfi  37756  mzpincl  37796  mzpcompact2lem  37813  wopprc  38095  dfac11  38130  kelac2  38133  pwslnmlem1  38160  pwslnm  38162  fvilbdRP  38479  brtrclfv2  38516  frege110  38764  frege133  38787  k0004lem3  38944  snelpwrVD  39557  fnchoice  39679  mpct  39877  elmapsnd  39880  difmapsn  39888  unirnmapsn  39890  ssmapsn  39892  limcresiooub  40351  limcresioolb  40352  cnfdmsn  40572  dvsinax  40604  fourierdlem48  40847  fourierdlem49  40848  salexct3  41036  salgencntex  41037  salgensscntex  41038  sge0sn  41072  sge0p1  41107  sge0xp  41122  ovnovollem1  41349  ovnovollem2  41350  vonvolmbllem  41353  setsv  41920  nnsum3primesprm  42250  mpt2exxg2  42681  mapsnop  42688  lindsrng01  42822  snlindsntorlem  42824  snlindsntor  42825  lmod1lem1  42841  lmod1lem2  42842  lmod1lem3  42843  lmod1lem4  42844  lmod1lem5  42845  lmod1  42846  lmod1zr  42847  aacllem  43115
  Copyright terms: Public domain W3C validator