Theorem snid 3761

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

Syntax hints:   e. wcel 1710  _Vcvv 2860  {csn 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-sn 3742

This theorem is referenced by:  rabsnt  3798  sneqr  3873  unsneqsn  3888  unipw  4118  eqpw1uni  4331  pw1eqadj  4333  0nelsuc  4401  0cnsuc  4402  nnsucelr  4429  nndisjeq  4430  ssfin  4471  eqtfinrelk  4487  0ceven  4506  vfinspss  4552  proj1op  4601  proj2op  4602  fsn  5433  fsn2  5435  fnressn  5439  fressnfv  5440  fvsn  5446  fvsnun1  5448  dmep  5525  map0  6026  mapsn  6027  xpsnen  6050  enadj  6061  2p1e3c  6157  frecxp  6315