Theorem snid 2439

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

Syntax hints:   e. wcel 960  Vcvv 1814  {csn 2413

This theorem is referenced by:  tpi3 2461  snnz 2462  sneqr 2481  el 2757  rext 2760  unipw 2762  opth1 2792  opprc3 2803  euuni 2887  reucl 2891  frirr 2930  sucid 3057  snsn0non 3131  opthprc 3227  fvsn 3800  fvsnun1 3801  fsn 3840  fsn2 3842  fnressn 3843  fressnfv 3844  tfrlem11 3927  mapsn 4351  0elixp 4366  elirrv 4607  infeq5 4630  kmlem2 4776  axpowndlem3 4963  xrsupss 6080  xrinfmss 6081  acdc3lem 7487  acdc2lem1 7489  acdclem 7495  grpsn 8120  ringsn 8159  hsn0elch 9115  ghomsn 10383  dtt2 10589  1ded 10642

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417

Copyright terms: Public domain