Theorem snss 2461

Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49.

Hypothesis

Ref	Expression
snss.1	|- A e. V

Assertion

Ref	Expression
snss	|- (A e. B <-> {A} (_ B)

Proof of Theorem snss

Step	Hyp	Ref	Expression
1		elsn 2421	. . . 4 |- (x e. {A} <-> x = A)
2	1	imbi1i 186	. . 3 |- ((x e. {A} -> x e. B) <-> (x = A -> x e. B))
3	2	albii 999	. 2 |- (A.x(x e. {A} -> x e. B) <-> A.x(x = A -> x e. B))
4		dfss2 2058	. 2 |- ({A} (_ B <-> A.x(x e. {A} -> x e. B))
5		snss.1	. . 3 |- A e. V
6	5	clel2 1891	. 2 |- (A e. B <-> A.x(x = A -> x e. B))
7	3, 4, 6	3bitr4r 184	1 |- (A e. B <-> {A} (_ B)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958  Vcvv 1811   (_ wss 2047  {csn 2409

This theorem is referenced by:  snssg 2463  snelpw 2752  sspwb 2755  nnullss 2768  exss 2769  pwssun 2827  rabsnt 2894  frirr 2924  fvimacnvi 3804  fvimacnv 3805  fvimacnvALT 3809  fnressn 3837  xpdom3 4445  limensuci 4506  zfregs 4647  xrsupss 6078  xrinfmss 6079  nn0ssz 6152  spansn 9480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053  df-sn 2412

Copyright terms: Public domain