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  4238  exmidexmid  4241  ss1o0el1  4242  exmidundif  4251  exmidundifim  4252  exmid1stab  4253  unipw  4262  intid  4269  ordtriexmidlem2  4569  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  regexmidlem1  4582  0elsucexmid  4614  ordpwsucexmid  4619  opthprc  4727  fsn  5754  fsn2  5756  fvsn  5781  fvsnun1  5783  acexmidlema  5937  acexmidlemb  5938  acexmidlemab  5940  brtpos0  6340  mapsn  6779  mapsncnv  6784  0elixp  6818  en1  6893  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djuf1olem  7157  exmidonfinlem  7303  elreal2  7945  1exp  10715  hashinfuni  10924  wrdexb  11008  0bits  12303  ennnfonelemhom  12819  dvef  15232  djucllem  15773  bj-d0clsepcl  15898