Theorem snssd 3764

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 3753	. . 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 2164   C_ wss 3154   {csn 3619

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160  df-ss 3167  df-sn 3625

This theorem is referenced by:  pwntru  4229  ecinxp  6666  xpdom3m  6890  ac6sfi  6956  undifdc  6982  iunfidisj  7007  fidcenumlemr  7016  ssfii  7035  en2other2  7258  un0addcl  9276  un0mulcl  9277  fseq1p1m1  10163  fsumge1  11607  fprodsplit1f  11780  phicl2  12355  ennnfonelemhf1o  12573  imasaddfnlemg  12900  imasaddflemg  12902  0subm  13059  gsumvallem2  13068  trivsubgd  13273  trivsubgsnd  13274  trivnsgd  13290  kerf1ghm  13347  lsssn0  13869  lss0ss  13870  lsptpcl  13893  lspsnvsi  13917  lspun0  13924  mulgrhm2  14109  zndvds  14148  rest0  14358  iscnp4  14397  cnconst2  14412  cnpdis  14421  txdis  14456  txdis1cn  14457  fsumcncntop  14746  dvef  14906  plyf  14916  elplyr  14919  elplyd  14920  ply1term  14922  plyaddlem  14928  plymullem  14929  plycolemc  14936  plycn  14940  bj-omtrans  15518  pwtrufal  15558