Theorem snid 3664

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

Syntax hints:   e. wcel 2176   _Vcvv 2772   {csn 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-sn 3639

This theorem is referenced by:  vsnid  3665  exsnrex  3675  rabsnt  3708  sneqr  3801  undifexmid  4237  exmidexmid  4240  ss1o0el1  4241  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  unipw  4261  intid  4268  ordtriexmidlem2  4568  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  regexmidlem1  4581  0elsucexmid  4613  ordpwsucexmid  4618  opthprc  4726  fsn  5752  fsn2  5754  fvsn  5779  fvsnun1  5781  acexmidlema  5935  acexmidlemb  5936  acexmidlemab  5938  brtpos0  6338  mapsn  6777  mapsncnv  6782  0elixp  6816  en1  6891  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djuf1olem  7155  exmidonfinlem  7301  elreal2  7943  1exp  10713  hashinfuni  10922  wrdexb  11006  0bits  12270  ennnfonelemhom  12786  dvef  15199  djucllem  15736  bj-d0clsepcl  15861