Theorem snss 2457

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 2417	. . . 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 997	. 2 |- (A.x(x e. {A} -> x e. B) <-> A.x(x = A -> x e. B))
4		dfss2 2054	. 2 |- ({A} (_ B <-> A.x(x e. {A} -> x e. B))
5		snss.1	. . 3 |- A e. V
6	5	clel2 1887	. 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 952   = wceq 954   e. wcel 956  Vcvv 1807   (_ wss 2043  {csn 2405

This theorem is referenced by:  snssg 2459  snelpw 2747  sspwb 2750  nnullss 2763  exss 2764  pwssun 2822  rabsnt 2889  frirr 2919  fvimacnvi 3795  fvimacnv 3796  fvimacnvALT 3800  fnressn 3828  xpdom3 4431  limensuci 4492  zfregs 4627  xrsupss 6033  xrinfmss 6034  nn0ssz 6107  spansn 9419

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-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-sn 2408

Copyright terms: Public domain