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

Theorem snex 4631
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4576. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)
Assertion
Ref Expression
snex  |-  { A }  e.  _V

Proof of Theorem snex
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfsn2 3988 . . 3  |-  { A }  =  { A ,  A }
2 preq12 4054 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 645 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2520 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4630 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 3126 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2543 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 4037 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 194 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4520 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2547 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 164 1  |-  { A }  e.  _V
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1370    e. wcel 1758   _Vcvv 3068   (/)c0 3735   {csn 3975   {cpr 3977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-v 3070  df-dif 3429  df-un 3431  df-nul 3736  df-sn 3976  df-pr 3978
This theorem is referenced by:  prex  4632  elALT  4633  dtruALT2  4634  snelpwi  4635  snelpw  4636  rext  4638  sspwb  4639  intid  4648  moabex  4649  nnullss  4652  exss  4653  opi1  4657  op1stb  4660  opnz  4661  opeqsn  4685  opeqpr  4686  opthwiener  4691  uniop  4692  frirr  4795  frsn  5007  onnev  5019  xpsspwOLD  5052  relop  5088  funopg  5548  tpex  6479  snnex  6482  difsnexi  6484  sucexb  6520  soex  6621  elxp4  6622  elxp5  6623  opabex3d  6655  opabex3  6656  1stval  6679  2ndval  6680  fo1st  6696  fo2nd  6697  mpt2exxg  6747  cnvf1o  6771  fnse  6789  suppsnop  6804  brtpos2  6851  tfrlem12  6948  tfrlem16  6952  mapsn  7354  fvdiagfn  7357  mapsnconst  7358  mapsncnv  7359  mapsnf1o2  7360  ralxpmap  7362  elixpsn  7402  ixpsnf1o  7403  mapsnf1o  7404  ensn1  7473  en1b  7477  mapsnen  7487  xpsnen  7495  endisj  7498  xpsnen2g  7504  domunsncan  7511  enfixsn  7520  domunsn  7561  fodomr  7562  disjenex  7569  domssex2  7571  domssex  7572  map2xp  7581  phplem2  7591  isinf  7627  pssnn  7632  findcard2  7653  ac6sfi  7657  xpfi  7684  fodomfi  7691  pwfilem  7706  fczfsuppd  7739  snopfsupp  7744  fisn  7778  marypha1lem  7784  brwdom2  7889  unxpwdom2  7904  elirrv  7913  epfrs  8052  tc2  8063  tcsni  8064  ranksuc  8173  fseqenlem1  8295  dfac5lem2  8395  dfac5lem3  8396  dfac5lem4  8397  kmlem2  8421  cdafn  8439  cdaval  8440  cdaassen  8452  mapcdaen  8454  cdadom1  8456  cdainf  8462  ackbij1lem5  8494  cfsuc  8527  isfin1-3  8656  hsmexlem4  8699  axcc2lem  8706  dcomex  8717  axdc3lem4  8723  axdc4lem  8725  ttukeylem3  8781  brdom7disj  8799  brdom6disj  8800  fpwwe2lem13  8910  canthwe  8919  canthp1lem1  8920  uniwun  9008  rankcf  9045  nn0ex  10686  hashge3el3dif  12289  hashxplem  12297  hashmap  12299  hashbclem  12307  hashf1lem1  12310  climconst2  13128  incexclem  13401  ramub1lem2  14190  cshwsex  14229  setsvalg  14299  setsid  14317  pwsbas  14527  pwsle  14532  pwssca  14536  pwssnf1o  14538  imasplusg  14557  imasmulr  14558  imasvsca  14560  imasip  14561  xpsc  14597  acsfn  14699  isfunc  14876  homaf  15000  homaval  15001  symg2bas  16005  idrespermg  16018  pmtrsn  16127  psgnsn  16128  gsum2d2  16571  gsumcom2  16572  dprdz  16632  dprdsn  16638  dprd2da  16646  pwssplit3  17248  drngnidl  17417  drnglpir  17441  evlssca  17715  mpfind  17729  evls1sca  17867  pf1ind  17898  frlmip  18312  islindf4  18376  mattposvs  18450  m1detdiag  18519  mdetrlin  18524  mdetrsca2  18526  mdetrlin2  18529  mdetunilem5  18538  smadiadetglem2  18594  basdif0  18674  ordtbas  18912  leordtval2  18932  dishaus  19102  discmp  19117  concompid  19151  dis2ndc  19180  dislly  19217  dis1stc  19219  1stckgen  19243  ptbasfi  19270  dfac14lem  19306  dfac14  19307  ptrescn  19328  xkoptsub  19343  pt1hmeo  19495  xpstopnlem1  19498  ptcmpfi  19502  isufil2  19597  ufileu  19608  filufint  19609  uffix  19610  uffixsn  19614  flimclslem  19673  ptcmplem1  19740  cnextfval  19750  imasdsf1olem  20064  icccmplem1  20515  icccmplem2  20516  rrxip  21010  elply2  21780  plyss  21783  plyeq0lem  21794  taylfval  21940  axlowdimlem15  23337  axlowdim  23342  umgra1  23395  uslgra1  23426  usgra1  23427  usgra1v  23443  cusgra1v  23504  uvtx01vtx  23535  wlkntrl  23596  0pthonv  23615  constr1trl  23622  1pthon  23625  1pthon2v  23627  1conngra  23696  vdgr1d  23708  vdgr1b  23709  vdgr1a  23711  grposn  23837  zrdivrng  24054  0ofval  24322  resf1o  26164  gsumle  26380  ordtconlem1  26488  esumpr  26650  esumfzf  26652  prsiga  26708  cntnevol  26776  eulerpartlemgs2  26897  ccatmulgnn0dir  27074  ofs1  27077  ofcs1  27078  subfacp1lem5  27206  erdszelem5  27217  erdszelem8  27220  cvmliftlem4  27311  cvmliftlem5  27312  cvmlift2lem6  27331  cvmlift2lem9  27334  cvmlift2lem12  27337  wfrlem15  27872  fobigcup  28065  elsingles  28083  fnsingle  28084  fvsingle  28085  dfiota3  28088  brapply  28103  brsuccf  28106  funpartlem  28107  altopthsn  28126  altxpsspw  28142  hfsn  28351  onpsstopbas  28410  finixpnum  28552  ptrest  28563  neibastop2lem  28719  topjoin  28724  fdc  28779  heiborlem3  28850  heiborlem8  28855  ismrer1  28875  elrfi  29168  mzpincl  29208  mzpcompact2lem  29226  wopprc  29517  dfac11  29553  kelac2  29556  pwslnmlem1  29583  pwslnm  29585  fnchoice  29889  mpt2exxg2  30866  mapsnop  30873  mat1dimelbas  31021  mat1dimscm  31025  mat1dimmul  31026  lindsrng01  31109  snlindsntorlem  31111  snlindsntor  31112  mnd1  31128  grp1  31129  abl1  31130  rng1  31132  rng1nnzr  31133  lmod1lem1  31136  lmod1lem2  31137  lmod1lem3  31138  lmod1lem4  31139  lmod1lem5  31140  lmod1  31141  lmod1zr  31142  snelpwrVD  31867  bnj918  32059  bnj95  32157  bnj1452  32343  bnj1489  32347  bj-sels  32755  bj-snsetex  32756  bj-elsngl  32761  bj-2uplex  32815  bj-elopg  32828  ldualset  33076  lineset  33688  ispointN  33692  dvaset  34955  dvhset  35032  dibval  35093  dibfna  35105
  Copyright terms: Public domain W3C validator