Theorem snid 3520

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

Syntax hints:   e. wcel 1461   _Vcvv 2655   {csn 3491

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-sn 3497

This theorem is referenced by:  vsnid  3521  exsnrex  3530  rabsnt  3562  sneqr  3651  undifexmid  4075  exmidexmid  4078  exmid01  4079  exmidundif  4087  exmidundifim  4088  unipw  4097  intid  4104  ordtriexmidlem2  4394  ordtriexmid  4395  ordtri2orexmid  4396  regexmidlem1  4406  0elsucexmid  4438  ordpwsucexmid  4443  opthprc  4548  fsn  5544  fsn2  5546  fvsn  5567  fvsnun1  5569  acexmidlema  5717  acexmidlemb  5718  acexmidlemab  5720  brtpos0  6101  mapsn  6536  mapsncnv  6541  0elixp  6575  en1  6645  djulclr  6884  djurclr  6885  djulcl  6886  djurcl  6887  djuf1olem  6888  elreal2  7559  1exp  10209  hashinfuni  10410  ennnfonelemhom  11767  djucllem  12690  bj-d0clsepcl  12806