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

Theorem snex 4188
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4168. (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 3628 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3682 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 629 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2324 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4187 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2818 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2342 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3669 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 188 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4124 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2346 . 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 1619    e. wcel 1621   _Vcvv 2763   (/)c0 3430   {csn 3614   {cpr 3615
This theorem is referenced by:  prex  4189  elALT  4190  dtruALT2  4191  snelpwi  4192  snelpw  4193  rext  4194  sspwb  4195  intid  4203  moabex  4204  nnullss  4207  exss  4208  opi1  4212  opnz  4214  opeqsn  4234  opeqpr  4235  opthwiener  4240  uniop  4241  frirr  4342  tpex  4491  snnex  4496  op1stb  4541  sucexb  4572  frsn  4748  onnev  4758  xpsspwOLD  4786  relop  4822  soex  5110  elxp4  5147  elxp5  5148  funopg  5225  opabex3  5703  1stval  6058  2ndval  6059  fo1st  6073  fo2nd  6074  mpt2exxg  6129  cnvf1o  6151  fnse  6166  brtpos2  6174  tposexg  6182  tfrlem12  6373  tfrlem16  6377  mapsn  6777  fvdiagfn  6780  mapsnconst  6781  mapsncnv  6782  mapsnf1o2  6783  elixpsn  6823  ixpsnf1o  6824  mapsnf1o  6825  ensn1  6893  en1b  6897  mapsnen  6906  xpsnen  6914  endisj  6917  xpsnen2g  6923  domunsncan  6930  domunsn  6979  fodomr  6980  disjenex  6987  domssex2  6989  domssex  6990  map2xp  6999  phplem2  7009  isinf  7044  pssnn  7049  findcard2  7066  ac6sfi  7069  xpfi  7096  fodomfi  7103  pwfilem  7118  fisn  7148  marypha1lem  7154  brwdom2  7255  unxpwdom2  7270  elirrv  7279  epfrs  7381  tc2  7395  tcsni  7396  ranksuc  7505  fseqenlem1  7619  dfac5lem2  7719  dfac5lem3  7720  dfac5lem4  7721  kmlem2  7745  cdafn  7763  cdaval  7764  cdaassen  7776  mapcdaen  7778  cdadom1  7780  cdainf  7786  ackbij1lem5  7818  cfsuc  7851  isfin1-3  7980  hsmexlem4  8023  axcc2lem  8030  dcomex  8041  axdc3lem4  8047  axdc4lem  8049  ttukeylem3  8106  brdom7disj  8124  brdom6disj  8125  fpwwe2lem13  8232  canthwe  8241  canthp1lem1  8242  uniwun  8330  rankcf  8367  nn0ex  9938  hashxplem  11350  hashmap  11352  hashbclem  11355  hashf1lem1  11358  climconst2  11987  ramub1lem2  13036  setsvalg  13133  setsid  13149  pwsbas  13348  pwsle  13353  pwssca  13357  pwssnf1o  13359  imasplusg  13382  imasmulr  13383  imasvsca  13385  xpsc  13421  acsfn  13523  isfunc  13700  homaf  13824  homaval  13825  gsum2d2  15187  gsumcom2  15188  dprdz  15227  dprdsn  15233  dprd2da  15239  drngnidl  15943  drnglpir  15967  basdif0  16653  ordtbas  16884  leordtval2  16904  dishaus  17072  discmp  17087  concompid  17119  dis2ndc  17148  dislly  17185  dis1stc  17187  1stckgen  17211  ptbasfi  17238  dfac14lem  17273  dfac14  17274  ptrescn  17295  xkoptsub  17310  pt1hmeo  17459  xpstopnlem1  17462  ptcmpfi  17466  isufil2  17565  ufileu  17576  filufint  17577  uffix  17578  uffixsn  17582  flimclslem  17641  ptcmplem1  17708  imasdsf1olem  17899  icccmplem1  18289  icccmplem2  18290  evlssca  19368  mpfind  19390  pf1ind  19400  elply2  19540  plyss  19543  plyeq0lem  19554  taylfval  19700  grposn  20842  zrdivrng  21059  0ofval  21325  subfacp1lem5  23087  erdszelem5  23098  erdszelem8  23101  cvmliftlem4  23191  cvmliftlem5  23192  cvmlift2lem6  23211  cvmlift2lem9  23214  cvmlift2lem12  23217  umgra1  23250  vdgr1d  23266  vdgr1b  23267  vdgr1a  23269  wfrlem15  23639  fobigcup  23816  elsingles  23832  fnsingle  23833  fvsingle  23834  brapply  23852  funpartfv  23858  altopthsn  23870  altxpsspw  23886  axlowdimlem15  23959  axlowdim  23964  hfsn  24184  onpsstopbas  24244  cbicp  24533  basexre  24889  1alg  25089  1ded  25105  1cat  25126  vtare  25252  smbkle  25410  neibastop2lem  25676  topjoin  25681  fdc  25822  heiborlem3  25904  heiborlem8  25909  ismrer1  25929  ralxpmap  26128  elrfi  26136  mzpincl  26179  mzpcompact2lem  26196  wopprc  26490  dfac11  26527  kelac2  26530  pwssplit3  26557  pwslnmlem1  26561  pwslnm  26563  enfixsn  26624  islindf4  26675  fnchoice  27068  snelpwrVD  27656  bnj918  27845  bnj95  27945  bnj153  27961  bnj1452  28131  bnj1489  28135  lsatset  28347  ldualset  28482  lineset  29094  ispointN  29098  dvaset  30361  dvhset  30438  dibval  30499  dibfna  30511
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-un 3132  df-nul 3431  df-sn 3620  df-pr 3621
  Copyright terms: Public domain W3C validator