Theorem snid 3563

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	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snid	⊢ 𝐴 ∈ {𝐴}

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 ⊢ 𝐴 ∈ V
2		snidb 3562	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 144	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 1481  Vcvv 2689  {csn 3532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-sn 3538

This theorem is referenced by:  vsnid  3564  exsnrex  3573  rabsnt  3606  sneqr  3695  undifexmid  4125  exmidexmid  4128  exmid01  4129  exmidundif  4137  exmidundifim  4138  unipw  4147  intid  4154  ordtriexmidlem2  4444  ordtriexmid  4445  ordtri2orexmid  4446  regexmidlem1  4456  0elsucexmid  4488  ordpwsucexmid  4493  opthprc  4598  fsn  5600  fsn2  5602  fvsn  5623  fvsnun1  5625  acexmidlema  5773  acexmidlemb  5774  acexmidlemab  5776  brtpos0  6157  mapsn  6592  mapsncnv  6597  0elixp  6631  en1  6701  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  djuf1olem  6946  exmidonfinlem  7066  elreal2  7662  1exp  10353  hashinfuni  10555  ennnfonelemhom  11964  dvef  12896  djucllem  13178  bj-d0clsepcl  13294  exmid1stab  13368