Theorem snid 3069

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.

Hypothesis

Ref	Expression
snid.1	|- A e. _V

Assertion

Ref	Expression
snid	|- A e. {A}

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 |- A e. _V
2		snidb 3068	. 2 |- (A e. _V <-> A e. {A})
3	1, 2	mpbi 206	1 |- A e. {A}

Syntax hints:   e. wcel 1300  _Vcvv 2292  {csn 3044

This theorem is referenced by:  tpid3OLD 3117  sneqr 3147  reucl 3213  elALT 3494  rext 3502  unipw 3504  intid 3512  opth1 3531  opprc3 3543  frirr 3634  sucidOLD 3745  sucidOLDOLD 3746  sucidOLDOLDOLD 3747  snsn0non 3788  snsn0nonOLD 3789  snnex 3801  euuni 3807  opthprc 4046  fvsn 4758  fvsnun1 4764  fsn 4807  fsn2 4809  fnressn 4812  fressnfv 4813  tfrlem11 5129  mapsn 5404  0elixp 5419  ac6sfilem3 5508  elirrv 5700  infeq5 5727  kmlem2 5928  axpowndlem3 6103  xrsupss 7287  xrinfmss 7288  acdc3lem 8754  acdc2lem1 8757  acdclem 8763  grpsn 9340  ringsn 9490  dif1enOLD 10173  indexfi 10174  zrdivrng 10418  hsn0elch 10753  bnj143 12475  bnj97 13220  bnj547 13273  bnj966 13348  bnj1442 13540  bnj1498 13562  ghomsn 13631  fvrn0 13837  wfrlem14 13970  wfrlem16 13972  limvinlv 14941  dtt2 14951  singempcon 14965  idtrgrp 14978  invtrgrp 14979  1ded 15085  alexsublem4 15440  locfindsc 15515  comppfsc 15517  ist1-2 15542  isufil2 15565  ufileu 15573  uffixfr 15575  ufinffr 15578  indexfiOLD 15755  zornn0 15764  heiborlem18 15972  bfp 16009  ismrer1 16024  grpkerinj 16042  0idl 16173  0ring 16175  snsslVD 16652  snssl 16653  unipwrVD 16656  unipwr 16657  sucidALTVD 16694  sucidALT 16695  sucidVD 16696

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-sn 3049

Copyright terms: Public domain