Theorem snidg 3458

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)

Assertion

Ref	Expression
snidg	|- ( A e. V -> A e. { A } )

Proof of Theorem snidg

Step	Hyp	Ref	Expression
1		eqid 2085	. 2 |- A = A
2		elsng 3446	. 2 |- ( A e. V -> ( A e. { A } <-> A = A ) )
3	1, 2	mpbiri 166	1 |- ( A e. V -> A e. { A } )

Syntax hints:   -> wi 4   = wceq 1287   e. wcel 1436   {csn 3431

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-sn 3437

This theorem is referenced by:  snidb  3459  elsn2g  3462  snnzg  3542  snmg  3543  fvunsng  5456  fsnunfv  5462  1stconst  5945  2ndconst  5946  tfr0dm  6043  tfrlemibxssdm  6048  tfrlemi14d  6054  tfr1onlembxssdm  6064  tfr1onlemres  6070  tfrcllembxssdm  6077  tfrcllemres  6083  en1uniel  6475  onunsnss  6581  snon0  6598  supsnti  6647  fseq1p1m1  9441  elfzomin  9548  fsumsplitsnun  10719  divalgmod  10852  bj-sels  11293