Theorem snid 3638

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

Syntax hints:   e. wcel 2160   _Vcvv 2752   {csn 3607

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-sn 3613

This theorem is referenced by:  vsnid  3639  exsnrex  3649  rabsnt  3682  sneqr  3775  undifexmid  4211  exmidexmid  4214  ss1o0el1  4215  exmidundif  4224  exmidundifim  4225  exmid1stab  4226  unipw  4235  intid  4242  ordtriexmidlem2  4537  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  regexmidlem1  4550  0elsucexmid  4582  ordpwsucexmid  4587  opthprc  4695  fsn  5709  fsn2  5711  fvsn  5732  fvsnun1  5734  acexmidlema  5888  acexmidlemb  5889  acexmidlemab  5891  brtpos0  6278  mapsn  6717  mapsncnv  6722  0elixp  6756  en1  6826  djulclr  7079  djurclr  7080  djulcl  7081  djurcl  7082  djuf1olem  7083  exmidonfinlem  7223  elreal2  7860  1exp  10583  hashinfuni  10792  ennnfonelemhom  12469  dvef  14665  djucllem  15030  bj-d0clsepcl  15155