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

Theorem snex 4215
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4195. (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
StepHypRef Expression
1 dfsn2 3655 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3709 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 629 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2350 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4214 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2844 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2368 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3696 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 188 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4151 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2372 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    = wceq 1628    e. wcel 1688   _Vcvv 2789   (/)c0 3456   {csn 3641   {cpr 3642
This theorem is referenced by:  prex  4216  elALT  4217  dtruALT2  4218  snelpwi  4219  snelpw  4220  rext  4221  sspwb  4222  intid  4230  moabex  4231  nnullss  4234  exss  4235  opi1  4239  opnz  4241  opeqsn  4261  opeqpr  4262  opthwiener  4267  uniop  4268  frirr  4369  tpex  4518  snnex  4523  op1stb  4568  sucexb  4599  frsn  4759  onnev  4769  xpsspwOLD  4797  relop  4833  soex  5121  elxp4  5158  elxp5  5159  funopg  5252  opabex3  5730  1stval  6085  2ndval  6086  fo1st  6100  fo2nd  6101  mpt2exxg  6156  cnvf1o  6178  fnse  6193  brtpos2  6201  tposexg  6209  tfrlem12  6400  tfrlem16  6404  mapsn  6804  fvdiagfn  6807  mapsnconst  6808  mapsncnv  6809  mapsnf1o2  6810  elixpsn  6850  ixpsnf1o  6851  mapsnf1o  6852  ensn1  6920  en1b  6924  mapsnen  6933  xpsnen  6941  endisj  6944  xpsnen2g  6950  domunsncan  6957  domunsn  7006  fodomr  7007  disjenex  7014  domssex2  7016  domssex  7017  map2xp  7026  phplem2  7036  isinf  7071  pssnn  7076  findcard2  7093  ac6sfi  7096  xpfi  7123  fodomfi  7130  pwfilem  7145  fisn  7175  marypha1lem  7181  brwdom2  7282  unxpwdom2  7297  elirrv  7306  epfrs  7408  tc2  7422  tcsni  7423  ranksuc  7532  fseqenlem1  7646  dfac5lem2  7746  dfac5lem3  7747  dfac5lem4  7748  kmlem2  7772  cdafn  7790  cdaval  7791  cdaassen  7803  mapcdaen  7805  cdadom1  7807  cdainf  7813  ackbij1lem5  7845  cfsuc  7878  isfin1-3  8007  hsmexlem4  8050  axcc2lem  8057  dcomex  8068  axdc3lem4  8074  axdc4lem  8076  ttukeylem3  8133  brdom7disj  8151  brdom6disj  8152  fpwwe2lem13  8259  canthwe  8268  canthp1lem1  8269  uniwun  8357  rankcf  8394  nn0ex  9966  hashxplem  11379  hashmap  11381  hashbclem  11384  hashf1lem1  11387  climconst2  12016  incexclem  12289  ramub1lem2  13068  setsvalg  13165  setsid  13181  pwsbas  13380  pwsle  13385  pwssca  13389  pwssnf1o  13391  imasplusg  13414  imasmulr  13415  imasvsca  13417  xpsc  13453  acsfn  13555  isfunc  13732  homaf  13856  homaval  13857  gsum2d2  15219  gsumcom2  15220  dprdz  15259  dprdsn  15265  dprd2da  15271  drngnidl  15975  drnglpir  15999  basdif0  16685  ordtbas  16916  leordtval2  16936  dishaus  17104  discmp  17119  concompid  17151  dis2ndc  17180  dislly  17217  dis1stc  17219  1stckgen  17243  ptbasfi  17270  dfac14lem  17305  dfac14  17306  ptrescn  17327  xkoptsub  17342  pt1hmeo  17491  xpstopnlem1  17494  ptcmpfi  17498  isufil2  17597  ufileu  17608  filufint  17609  uffix  17610  uffixsn  17614  flimclslem  17673  ptcmplem1  17740  imasdsf1olem  17931  icccmplem1  18321  icccmplem2  18322  evlssca  19400  mpfind  19422  pf1ind  19432  elply2  19572  plyss  19575  plyeq0lem  19586  taylfval  19732  grposn  20874  zrdivrng  21091  0ofval  21357  subfacp1lem5  23119  erdszelem5  23130  erdszelem8  23133  cvmliftlem4  23223  cvmliftlem5  23224  cvmlift2lem6  23243  cvmlift2lem9  23246  cvmlift2lem12  23249  umgra1  23282  vdgr1d  23298  vdgr1b  23299  vdgr1a  23301  wfrlem15  23671  fobigcup  23848  elsingles  23864  fnsingle  23865  fvsingle  23866  brapply  23884  funpartfv  23890  altopthsn  23902  altxpsspw  23918  axlowdimlem15  23991  axlowdim  23996  hfsn  24216  onpsstopbas  24276  cbicp  24565  basexre  24921  1alg  25121  1ded  25137  1cat  25158  vtare  25284  smbkle  25442  neibastop2lem  25708  topjoin  25713  fdc  25854  heiborlem3  25936  heiborlem8  25941  ismrer1  25961  ralxpmap  26160  elrfi  26168  mzpincl  26211  mzpcompact2lem  26228  wopprc  26522  dfac11  26559  kelac2  26562  pwssplit3  26589  pwslnmlem1  26593  pwslnm  26595  enfixsn  26656  islindf4  26707  fnchoice  27099  snelpwrVD  27874  bnj918  28063  bnj95  28163  bnj153  28179  bnj1452  28349  bnj1489  28353  lsatset  28447  ldualset  28582  lineset  29194  ispointN  29198  dvaset  30461  dvhset  30538  dibval  30599  dibfna  30611
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-un 3158  df-nul 3457  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator