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

Theorem snex 4216
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4196. (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 3654 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3708 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 626 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2349 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4215 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2843 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2367 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3695 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 186 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4150 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2371 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 156 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1623    e. wcel 1684   _Vcvv 2788   (/)c0 3455   {csn 3640   {cpr 3641
This theorem is referenced by:  prex  4217  elALT  4218  dtruALT2  4219  snelpwi  4220  snelpw  4221  rext  4222  sspwb  4223  intid  4231  moabex  4232  nnullss  4235  exss  4236  opi1  4240  opnz  4242  opeqsn  4262  opeqpr  4263  opthwiener  4268  uniop  4269  frirr  4370  tpex  4519  snnex  4524  op1stb  4569  sucexb  4600  frsn  4760  onnev  4770  xpsspwOLD  4798  relop  4834  soex  5122  elxp4  5160  elxp5  5161  funopg  5286  opabex3  5769  1stval  6124  2ndval  6125  fo1st  6139  fo2nd  6140  mpt2exxg  6195  cnvf1o  6217  fnse  6232  brtpos2  6240  tposexg  6248  tfrlem12  6405  tfrlem16  6409  mapsn  6809  fvdiagfn  6812  mapsnconst  6813  mapsncnv  6814  mapsnf1o2  6815  elixpsn  6855  ixpsnf1o  6856  mapsnf1o  6857  ensn1  6925  en1b  6929  mapsnen  6938  xpsnen  6946  endisj  6949  xpsnen2g  6955  domunsncan  6962  domunsn  7011  fodomr  7012  disjenex  7019  domssex2  7021  domssex  7022  map2xp  7031  phplem2  7041  isinf  7076  pssnn  7081  findcard2  7098  ac6sfi  7101  xpfi  7128  fodomfi  7135  pwfilem  7150  fisn  7180  marypha1lem  7186  brwdom2  7287  unxpwdom2  7302  elirrv  7311  epfrs  7413  tc2  7427  tcsni  7428  ranksuc  7537  fseqenlem1  7651  dfac5lem2  7751  dfac5lem3  7752  dfac5lem4  7753  kmlem2  7777  cdafn  7795  cdaval  7796  cdaassen  7808  mapcdaen  7810  cdadom1  7812  cdainf  7818  ackbij1lem5  7850  cfsuc  7883  isfin1-3  8012  hsmexlem4  8055  axcc2lem  8062  dcomex  8073  axdc3lem4  8079  axdc4lem  8081  ttukeylem3  8138  brdom7disj  8156  brdom6disj  8157  fpwwe2lem13  8264  canthwe  8273  canthp1lem1  8274  uniwun  8362  rankcf  8399  nn0ex  9971  hashxplem  11385  hashmap  11387  hashbclem  11390  hashf1lem1  11393  climconst2  12022  incexclem  12295  ramub1lem2  13074  setsvalg  13171  setsid  13187  pwsbas  13386  pwsle  13391  pwssca  13395  pwssnf1o  13397  imasplusg  13420  imasmulr  13421  imasvsca  13423  xpsc  13459  acsfn  13561  isfunc  13738  homaf  13862  homaval  13863  gsum2d2  15225  gsumcom2  15226  dprdz  15265  dprdsn  15271  dprd2da  15277  drngnidl  15981  drnglpir  16005  basdif0  16691  ordtbas  16922  leordtval2  16942  dishaus  17110  discmp  17125  concompid  17157  dis2ndc  17186  dislly  17223  dis1stc  17225  1stckgen  17249  ptbasfi  17276  dfac14lem  17311  dfac14  17312  ptrescn  17333  xkoptsub  17348  pt1hmeo  17497  xpstopnlem1  17500  ptcmpfi  17504  isufil2  17603  ufileu  17614  filufint  17615  uffix  17616  uffixsn  17620  flimclslem  17679  ptcmplem1  17746  imasdsf1olem  17937  icccmplem1  18327  icccmplem2  18328  evlssca  19406  mpfind  19428  pf1ind  19438  elply2  19578  plyss  19581  plyeq0lem  19592  taylfval  19738  grposn  20882  zrdivrng  21099  0ofval  21365  cntnevol  23175  esumpr  23438  prsiga  23492  subfacp1lem5  23715  erdszelem5  23726  erdszelem8  23729  cvmliftlem4  23819  cvmliftlem5  23820  cvmlift2lem6  23839  cvmlift2lem9  23842  cvmlift2lem12  23845  umgra1  23878  vdgr1d  23894  vdgr1b  23895  vdgr1a  23897  wfrlem15  24270  fobigcup  24440  elsingles  24457  fnsingle  24458  fvsingle  24459  dfiota3  24462  brapply  24477  brsuccf  24480  funpartfun  24481  funpartfv  24483  altopthsn  24495  altxpsspw  24511  axlowdimlem15  24584  axlowdim  24589  hfsn  24809  onpsstopbas  24869  cbicp  25166  basexre  25522  1alg  25722  1ded  25738  1cat  25759  vtare  25885  smbkle  26043  cndpv  26049  pgapspf  26052  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  neibastop2lem  26309  topjoin  26314  fdc  26455  heiborlem3  26537  heiborlem8  26542  ismrer1  26562  ralxpmap  26761  elrfi  26769  mzpincl  26812  mzpcompact2lem  26829  wopprc  27123  dfac11  27160  kelac2  27163  pwssplit3  27190  pwslnmlem1  27194  pwslnm  27196  enfixsn  27257  islindf4  27308  fnchoice  27700  uslgra1  28118  usgra1  28119  usgra1v  28126  cusgra1v  28157  uvtx01vtx  28164  snelpwrVD  28606  bnj918  28796  bnj95  28896  bnj153  28912  bnj1452  29082  bnj1489  29086  lsatset  29180  ldualset  29315  lineset  29927  ispointN  29931  dvaset  31194  dvhset  31271  dibval  31332  dibfna  31344
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator