Theorem snid 2431

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.

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 2430	. 2 |- (A e. V <-> A e. {A})
3	1, 2	mpbi 189	1 |- A e. {A}

Syntax hints:   e. wcel 956  Vcvv 1807  {csn 2405

This theorem is referenced by:  tpi3 2453  snnz 2454  sneqr 2473  el 2746  rext 2749  unipw 2751  opth1 2781  opprc3 2792  euuni 2876  reucl 2880  frirr 2919  sucid 3046  snsn0non 3120  opthprc 3216  fvsn 3785  fvsnun1 3786  fsn 3825  fsn2 3827  fnressn 3828  fressnfv 3829  tfrlem11 3912  mapsn 4335  0elixp 4350  elirrv 4578  infeq5 4601  kmlem2 4746  axpowndlem3 4931  xrsupss 6033  xrinfmss 6034  acdc3lem 7436  acdc2lem1 7438  acdclem 7444  grpsn 8076  ringsn 8115  hsn0elch 9059  ghomsn 10322  dtt2 10498  1ded 10551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409

Copyright terms: Public domain