Theorem snid 3700

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

Syntax hints:   e. wcel 2202   _Vcvv 2802   {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  vsnid  3701  exsnrex  3711  rabsnt  3746  sneqr  3843  undifexmid  4283  exmidexmid  4286  ss1o0el1  4287  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  unipw  4309  intid  4316  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  regexmidlem1  4631  0elsucexmid  4663  ordpwsucexmid  4668  opthprc  4777  fsn  5819  fsn2  5821  fvsn  5848  fvsnun1  5850  acexmidlema  6008  acexmidlemb  6009  acexmidlemab  6011  brtpos0  6417  mapsn  6858  mapsncnv  6863  0elixp  6897  en1  6972  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djuf1olem  7251  exmidonfinlem  7403  elreal2  8049  1exp  10829  hashinfuni  11038  wrdexb  11124  0bits  12519  ennnfonelemhom  13035  dvef  15450  wlkl1loop  16208  djucllem  16396  bj-d0clsepcl  16520