Theorem snssd 3860

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 3849	. . 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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   e. wcel 2209   C_ wss 3220   {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-sn 3715

This theorem is used by:  pwntru  4338  ecinxp  6889  mapm  6975  xpdom3m  7138  ac6sfi  7208  undifdc  7237  iunfidisj  7266  fidcenumlemr  7279  ssfii  7313  en2other2  7554  pw1m  7589  un0addcl  9607  un0mulcl  9608  fseq1p1m1  10517  hashfibclem  11303  hashf1lem1  11306  hashf1lem2  11307  fsumge1  12252  fprodsplit1f  12425  bitsinv1  12753  phicl2  13020  ennnfonelemhf1o  13361  imasaddfnlemg  13693  imasaddflemg  13695  0subm  13849  gsumvallem2  13858  trivsubgd  14061  trivsubgsnd  14062  trivnsgd  14078  kerf1ghm  14135  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsumresfi  14262  gsum2dfilem2  14271  lsssn0  14815  lss0ss  14816  lsptpcl  14839  lspsnvsi  14863  lspun0  14870  mulgrhm2  15053  zndvds  15092  psrlidmfi  15208  psrridmfi  15209  mvrclfi  15226  rest0  15422  iscnp4  15461  cnconst2  15476  cnpdis  15485  txdis  15520  txdis1cn  15521  fsumcncntop  15810  dvef  15970  plyf  15980  elplyr  15983  elplyd  15984  ply1term  15986  plyaddlem  15992  plymullem  15993  plycolemc  16001  plycn  16005  dvply2g  16009  ppiprm  16276  chtprm  16278  perfectlem2  16317  upgr1elem1  16583  bj-omtrans  17204  pwtrufal  17249