Theorem snid 3470

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)

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 3469	. 2 |- ( A e. _V <-> A e. { A } )
3	1, 2	mpbi 143	1 |- A e. { A }

Syntax hints:   e. wcel 1438   _Vcvv 2619   {csn 3441

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-sn 3447

This theorem is referenced by:  vsnid  3471  exsnrex  3480  rabsnt  3512  sneqr  3599  undifexmid  4019  exmidexmid  4022  exmid01  4023  exmidundif  4026  unipw  4035  intid  4042  ordtriexmidlem2  4327  ordtriexmid  4328  ordtri2orexmid  4329  regexmidlem1  4339  0elsucexmid  4371  ordpwsucexmid  4376  opthprc  4477  fsn  5453  fsn2  5455  fvsn  5476  fvsnun1  5478  acexmidlema  5625  acexmidlemb  5626  acexmidlemab  5628  brtpos0  5999  mapsn  6427  mapsncnv  6432  en1  6496  djulclr  6720  djurclr  6721  djulcl  6722  djurcl  6723  djuf1olem  6724  elreal2  7347  1exp  9949  hashinfuni  10150  djucllem  11357  bj-d0clsepcl  11477