Theorem snssd 3768

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
snssd.1	|- ( ph -> A e. B )

Assertion

Ref	Expression
snssd	|- ( ph -> { A } C_ B )

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 |- ( ph -> A e. B )
2		snssg 3757	. . 3 |- ( A e. B -> ( A e. B <-> { A } C_ B ) )
3	1, 2	syl 14	. 2 |- ( ph -> ( A e. B <-> { A } C_ B ) )
4	1, 3	mpbid 147	1 |- ( ph -> { A } C_ B )

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2167   C_ wss 3157   {csn 3623

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170  df-sn 3629

This theorem is referenced by:  pwntru  4233  ecinxp  6678  xpdom3m  6902  ac6sfi  6968  undifdc  6994  iunfidisj  7021  fidcenumlemr  7030  ssfii  7049  en2other2  7275  un0addcl  9299  un0mulcl  9300  fseq1p1m1  10186  fsumge1  11643  fprodsplit1f  11816  bitsinv1  12144  phicl2  12407  ennnfonelemhf1o  12655  imasaddfnlemg  13016  imasaddflemg  13018  0subm  13186  gsumvallem2  13195  trivsubgd  13406  trivsubgsnd  13407  trivnsgd  13423  kerf1ghm  13480  lsssn0  14002  lss0ss  14003  lsptpcl  14026  lspsnvsi  14050  lspun0  14057  mulgrhm2  14242  zndvds  14281  rest0  14499  iscnp4  14538  cnconst2  14553  cnpdis  14562  txdis  14597  txdis1cn  14598  fsumcncntop  14887  dvef  15047  plyf  15057  elplyr  15060  elplyd  15061  ply1term  15063  plyaddlem  15069  plymullem  15070  plycolemc  15078  plycn  15082  dvply2g  15086  perfectlem2  15320  bj-omtrans  15686  pwtrufal  15728