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

Theorem snex 5045
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4989. (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 4322 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4402 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 680 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2812 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 5044 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3394 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2831 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4385 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 206 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4930 . . 3 ∅ ∈ V
119, 10syl6eqel 2835 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 176 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1620  wcel 2127  Vcvv 3328  c0 4046  {csn 4309  {cpr 4311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-dif 3706  df-un 3708  df-nul 4047  df-sn 4310  df-pr 4312
This theorem is referenced by:  prex  5046  elALT  5047  dtruALT2  5048  snelpwi  5049  snelpw  5050  rext  5053  sspwb  5054  intid  5063  moabex  5064  nnullss  5067  exss  5068  elopg  5071  opi1  5073  op1stb  5076  opnz  5078  opeqsn  5103  opeqpr  5104  opthwiener  5112  uniop  5113  0sn0ep  5171  frirr  5231  frsn  5334  xpsspw  5377  relop  5416  onnev  5997  funopg  6071  funsneqopsn  6568  funsneqop  6569  fsnex  6689  tpex  7110  snnex  7119  snnexOLD  7120  difsnexi  7123  sucexb  7162  soex  7262  elxp4  7263  elxp5  7264  opabex3d  7298  opabex3  7299  1stval  7323  2ndval  7324  fo1st  7341  fo2nd  7342  mpt2exxg  7400  cnvf1o  7432  fnse  7450  suppsnop  7465  brtpos2  7515  wfrlem15  7586  tfrlem12  7642  tfrlem16  7646  mapsn  8053  fvdiagfn  8056  mapsnconst  8057  mapsncnv  8058  mapsnf1o2  8059  ralxpmap  8061  elixpsn  8101  ixpsnf1o  8102  mapsnf1o  8103  ensn1  8173  en1b  8177  mapsnen  8188  xpsnen  8197  endisj  8200  xpsnen2g  8206  domunsncan  8213  enfixsn  8222  domunsn  8263  fodomr  8264  disjenex  8271  domssex2  8273  domssex  8274  map2xp  8283  phplem2  8293  isinf  8326  pssnn  8331  findcard2  8353  ac6sfi  8357  xpfi  8384  fodomfi  8392  pwfilem  8413  fczfsuppd  8446  snopfsupp  8451  fisn  8486  marypha1lem  8492  brwdom2  8631  unxpwdom2  8646  elirrv  8654  epfrs  8768  tc2  8779  tcsni  8780  ranksuc  8889  fseqenlem1  9008  dfac5lem2  9108  dfac5lem3  9109  dfac5lem4  9110  kmlem2  9136  cdafn  9154  cdaval  9155  cdaassen  9167  mapcdaen  9169  cdadom1  9171  cdainf  9177  ackbij1lem5  9209  cfsuc  9242  isfin1-3  9371  hsmexlem4  9414  axcc2lem  9421  dcomex  9432  axdc3lem4  9438  axdc4lem  9440  ttukeylem3  9496  brdom7disj  9516  brdom6disj  9517  fpwwe2lem13  9627  canthwe  9636  canthp1lem1  9637  uniwun  9725  rankcf  9762  nn0ex  11461  hashxplem  13383  hashmap  13385  hashbclem  13399  hashf1lem1  13402  hashge3el3dif  13431  ofs1  13881  climconst2  14449  incexclem  14738  ramub1lem2  15904  cshwsex  15980  setsvalg  16060  setsid  16087  pwsbas  16320  pwsle  16325  pwssca  16329  pwssnf1o  16331  imasplusg  16350  imasmulr  16351  imasvsca  16353  imasip  16354  xpsc  16390  acsfn  16492  isfunc  16696  homaf  16852  homaval  16853  funcsetcestrclem1  16966  mgm1  17429  sgrp1  17465  mnd1  17503  mnd1id  17504  grp1  17694  grp1inv  17695  symg2bas  17989  idrespermg  18002  pmtrsn  18110  psgnsn  18111  abl1  18440  gsum2d2  18544  gsumcom2  18545  dprdz  18600  dprdsn  18606  dprd2da  18612  ring1  18773  pwssplit3  19234  drngnidl  19402  drnglpir  19426  rng1nnzr  19447  evlssca  19695  mpfind  19709  evls1sca  19861  pf1ind  19892  frlmip  20290  islindf4  20350  mattposvs  20434  mat1dimelbas  20450  mat1dimscm  20454  mat1dimmul  20455  mat1rhmval  20458  m1detdiag  20576  mdetrlin  20581  mdetrsca2  20583  mdetrlin2  20586  mdetunilem5  20595  smadiadetglem2  20651  basdif0  20930  ordtbas  21169  leordtval2  21189  dishaus  21359  discmp  21374  conncompid  21407  dis2ndc  21436  dislly  21473  dis1stc  21475  unisngl  21503  1stckgen  21530  ptbasfi  21557  dfac14lem  21593  dfac14  21594  ptrescn  21615  xkoptsub  21630  pt1hmeo  21782  xpstopnlem1  21785  ptcmpfi  21789  isufil2  21884  ufileu  21895  filufint  21896  uffix  21897  uffixsn  21901  flimclslem  21960  ptcmplem1  22028  cnextfval  22038  imasdsf1olem  22350  icccmplem1  22797  icccmplem2  22798  rrxip  23349  elply2  24122  plyss  24125  plyeq0lem  24136  taylfval  24283  axlowdimlem15  26006  axlowdim  26011  snstriedgval  26100  vtxvalsnop  26103  iedgvalsnop  26104  upgr1eop  26180  upgr1eopALT  26182  uspgr1eop  26309  usgr1eop  26312  lfuhgr1v0e  26316  1loopgrvd2  26580  1loopgrvd0  26581  p1evtxdeqlem  26589  p1evtxdeq  26590  p1evtxdp1  26591  uspgrloopvtx  26592  uspgrloopiedg  26594  uspgrloopedg  26595  wlkp1lem4  26754  0pthonv  27252  eupth2lem3  27359  wlkl0  27499  0ofval  27922  resf1o  29785  ordtconnlem1  30250  esumpr  30408  esumrnmpt2  30410  esumfzf  30411  esum2dlem  30434  esum2d  30435  esumiun  30436  prsiga  30474  rossros  30523  cntnevol  30571  carsgclctunlem1  30659  omsmeas  30665  eulerpartlemgs2  30722  ccatmulgnn0dir  30899  ofcs1  30901  actfunsnf1o  30962  actfunsnrndisj  30963  reprsuc  30973  breprexplema  30988  bnj918  31114  bnj95  31212  bnj1452  31398  bnj1489  31402  subfacp1lem5  31444  erdszelem5  31455  erdszelem8  31458  cvmliftlem4  31548  cvmliftlem5  31549  cvmlift2lem6  31568  cvmlift2lem9  31571  cvmlift2lem12  31574  conway  32187  etasslt  32197  slerec  32200  fobigcup  32284  elsingles  32302  fnsingle  32303  fvsingle  32304  dfiota3  32307  brapply  32322  brsuccf  32325  funpartlem  32326  altopthsn  32345  altxpsspw  32361  hfsn  32563  neibastop2lem  32632  topjoin  32637  onpsstopbas  32706  bj-sels  33227  bj-snsetex  33228  bj-elsngl  33233  bj-2uplex  33287  bj-restsn  33312  bj-snmoore  33345  f1omptsnlem  33465  mptsnunlem  33467  topdifinffinlem  33477  finixpnum  33676  ptrest  33690  poimirlem3  33694  poimirlem4  33695  poimirlem28  33719  fdc  33823  heiborlem3  33894  heiborlem8  33899  ismrer1  33919  grposnOLD  33963  zrdivrng  34034  ldualset  34884  lineset  35496  ispointN  35500  dvaset  36764  dvhset  36841  dibval  36902  dibfna  36914  elrfi  37728  mzpincl  37768  mzpcompact2lem  37785  wopprc  38068  dfac11  38103  kelac2  38106  pwslnmlem1  38133  pwslnm  38135  fvilbdRP  38453  brtrclfv2  38490  frege110  38738  frege133  38761  k0004lem3  38918  snelpwrVD  39534  fnchoice  39656  mapsnd  39856  mapsnend  39859  mpct  39861  elmapsnd  39864  difmapsn  39872  unirnmapsn  39874  ssmapsn  39876  limcresiooub  40346  limcresioolb  40347  cnfdmsn  40567  dvsinax  40599  fourierdlem48  40843  fourierdlem49  40844  salexct3  41032  salgencntex  41033  salgensscntex  41034  sge0sn  41068  sge0p1  41103  sge0xp  41118  ovnovollem1  41345  ovnovollem2  41346  vonvolmbllem  41349  setsv  41827  nnsum3primesprm  42157  mpt2exxg2  42595  mapsnop  42602  lindsrng01  42736  snlindsntorlem  42738  snlindsntor  42739  lmod1lem1  42755  lmod1lem2  42756  lmod1lem3  42757  lmod1lem4  42758  lmod1lem5  42759  lmod1  42760  lmod1zr  42761  aacllem  43029
  Copyright terms: Public domain W3C validator