Theorem snidg 3520

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 2115	. 2 |- A = A
2		elsng 3508	. 2 |- ( A e. V -> ( A e. { A } <-> A = A ) )
3	1, 2	mpbiri 167	1 |- ( A e. V -> A e. { A } )

Syntax hints:   -> wi 4   = wceq 1314   e. wcel 1463   {csn 3493

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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-sn 3499

This theorem is referenced by:  snidb  3521  elsn2g  3524  snnzg  3606  snmg  3607  exmidsssnc  4086  fvunsng  5568  fsnunfv  5575  1stconst  6072  2ndconst  6073  tfr0dm  6173  tfrlemibxssdm  6178  tfrlemi14d  6184  tfr1onlembxssdm  6194  tfr1onlemres  6200  tfrcllembxssdm  6207  tfrcllemres  6213  en1uniel  6652  onunsnss  6758  snon0  6776  supsnti  6844  fseq1p1m1  9764  elfzomin  9873  fsumsplitsnun  11077  divalgmod  11469  setsslid  11849  1strbas  11898  srnginvld  11925  lmodvscad  11936  cnpdis  12250  bj-sels  12796