Theorem snid 3624

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 3623	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 145	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2148  Vcvv 2738  {csn 3593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-sn 3599

This theorem is referenced by:  vsnid  3625  exsnrex  3635  rabsnt  3668  sneqr  3761  undifexmid  4194  exmidexmid  4197  ss1o0el1  4198  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  unipw  4218  intid  4225  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  regexmidlem1  4533  0elsucexmid  4565  ordpwsucexmid  4570  opthprc  4678  fsn  5689  fsn2  5691  fvsn  5712  fvsnun1  5714  acexmidlema  5866  acexmidlemb  5867  acexmidlemab  5869  brtpos0  6253  mapsn  6690  mapsncnv  6695  0elixp  6729  en1  6799  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djuf1olem  7052  exmidonfinlem  7192  elreal2  7829  1exp  10549  hashinfuni  10757  ennnfonelemhom  12416  dvef  14191  djucllem  14555  bj-d0clsepcl  14680