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

Theorem snex 4392
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4372. (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 3815 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3872 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 627 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2496 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4391 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2998 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2514 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3858 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 187 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4326 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2518 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1652    e. wcel 1725   _Vcvv 2943   (/)c0 3615   {csn 3801   {cpr 3802
This theorem is referenced by:  prex  4393  elALT  4394  dtruALT2  4395  snelpwi  4396  snelpw  4397  rext  4399  sspwb  4400  intid  4408  moabex  4409  nnullss  4412  exss  4413  opi1  4417  opnz  4419  opeqsn  4439  opeqpr  4440  opthwiener  4445  uniop  4446  frirr  4546  tpex  4694  snnex  4699  op1stb  4744  sucexb  4775  frsn  4934  onnev  4944  xpsspwOLD  4973  relop  5009  soex  5305  elxp4  5343  elxp5  5344  funopg  5471  opabex3d  5975  opabex3  5976  1stval  6337  2ndval  6338  fo1st  6352  fo2nd  6353  mpt2exxg  6408  cnvf1o  6431  fnse  6449  brtpos2  6471  tfrlem12  6636  tfrlem16  6640  mapsn  7041  fvdiagfn  7044  mapsnconst  7045  mapsncnv  7046  mapsnf1o2  7047  elixpsn  7087  ixpsnf1o  7088  mapsnf1o  7089  ensn1  7157  en1b  7161  mapsnen  7170  xpsnen  7178  endisj  7181  xpsnen2g  7187  domunsncan  7194  domunsn  7243  fodomr  7244  disjenex  7251  domssex2  7253  domssex  7254  map2xp  7263  phplem2  7273  isinf  7308  pssnn  7313  findcard2  7334  ac6sfi  7337  xpfi  7364  fodomfi  7371  pwfilem  7387  fisn  7418  marypha1lem  7424  brwdom2  7525  unxpwdom2  7540  elirrv  7549  epfrs  7651  tc2  7665  tcsni  7666  ranksuc  7775  fseqenlem1  7889  dfac5lem2  7989  dfac5lem3  7990  dfac5lem4  7991  kmlem2  8015  cdafn  8033  cdaval  8034  cdaassen  8046  mapcdaen  8048  cdadom1  8050  cdainf  8056  ackbij1lem5  8088  cfsuc  8121  isfin1-3  8250  hsmexlem4  8293  axcc2lem  8300  dcomex  8311  axdc3lem4  8317  axdc4lem  8319  ttukeylem3  8375  brdom7disj  8393  brdom6disj  8394  fpwwe2lem13  8501  canthwe  8510  canthp1lem1  8511  uniwun  8599  rankcf  8636  nn0ex  10211  hashxplem  11679  hashmap  11681  hashbclem  11684  hashf1lem1  11687  climconst2  12325  incexclem  12599  ramub1lem2  13378  setsvalg  13475  setsid  13491  pwsbas  13692  pwsle  13697  pwssca  13701  pwssnf1o  13703  imasplusg  13726  imasmulr  13727  imasvsca  13729  xpsc  13765  acsfn  13867  isfunc  14044  homaf  14168  homaval  14169  gsum2d2  15531  gsumcom2  15532  dprdz  15571  dprdsn  15577  dprd2da  15583  drngnidl  16283  drnglpir  16307  basdif0  17001  ordtbas  17239  leordtval2  17259  dishaus  17429  discmp  17444  concompid  17477  dis2ndc  17506  dislly  17543  dis1stc  17545  1stckgen  17569  ptbasfi  17596  dfac14lem  17632  dfac14  17633  ptrescn  17654  xkoptsub  17669  pt1hmeo  17821  xpstopnlem1  17824  ptcmpfi  17828  isufil2  17923  ufileu  17934  filufint  17935  uffix  17936  uffixsn  17940  flimclslem  17999  ptcmplem1  18066  cnextfval  18076  imasdsf1olem  18386  icccmplem1  18836  icccmplem2  18837  evlssca  19926  mpfind  19948  pf1ind  19958  elply2  20098  plyss  20101  plyeq0lem  20112  taylfval  20258  umgra1  21344  uslgra1  21375  usgra1  21376  usgra1v  21392  cusgra1v  21453  uvtx01vtx  21484  wlkntrl  21545  0pthonv  21564  constr1trl  21571  1pthon  21574  1pthon2v  21576  1conngra  21645  vdgr1d  21657  vdgr1b  21658  vdgr1a  21660  grposn  21786  zrdivrng  22003  0ofval  22271  esumpr  24440  esumfzf  24442  prsiga  24497  cntnevol  24565  subfacp1lem5  24853  erdszelem5  24864  erdszelem8  24867  cvmliftlem4  24958  cvmliftlem5  24959  cvmlift2lem6  24978  cvmlift2lem9  24981  cvmlift2lem12  24984  wfrlem15  25520  fobigcup  25690  elsingles  25708  fnsingle  25709  fvsingle  25710  dfiota3  25713  brapply  25728  brsuccf  25731  funpartlem  25732  altopthsn  25749  altxpsspw  25765  axlowdimlem15  25838  axlowdim  25843  hfsn  26063  onpsstopbas  26123  neibastop2lem  26321  topjoin  26326  fdc  26381  heiborlem3  26454  heiborlem8  26459  ismrer1  26479  ralxpmap  26674  elrfi  26680  mzpincl  26723  mzpcompact2lem  26740  wopprc  27033  dfac11  27070  kelac2  27073  pwssplit3  27100  pwslnmlem1  27104  pwslnm  27106  enfixsn  27167  islindf4  27218  fnchoice  27609  snelpwrVD  28695  bnj918  28887  bnj95  28987  bnj1452  29173  bnj1489  29177  ldualset  29654  lineset  30266  ispointN  30270  dvaset  31533  dvhset  31610  dibval  31671  dibfna  31683
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-v 2945  df-dif 3310  df-un 3312  df-nul 3616  df-sn 3807  df-pr 3808
  Copyright terms: Public domain W3C validator