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  4336  ecinxp  6884  xpdom3m  7132  ac6sfi  7202  undifdc  7231  iunfidisj  7260  fidcenumlemr  7272  ssfii  7308  en2other2  7548  pw1m  7583  un0addcl  9596  un0mulcl  9597  fseq1p1m1  10501  hashfibclem  11282  hashf1lem1  11285  hashf1lem2  11286  fsumge1  12228  fprodsplit1f  12401  bitsinv1  12729  phicl2  12992  ennnfonelemhf1o  13304  imasaddfnlemg  13635  imasaddflemg  13637  0subm  13791  gsumvallem2  13800  trivsubgd  14003  trivsubgsnd  14004  trivnsgd  14020  kerf1ghm  14077  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  lsssn0  14707  lss0ss  14708  lsptpcl  14731  lspsnvsi  14755  lspun0  14762  mulgrhm2  14945  zndvds  14984  rest0  15280  iscnp4  15319  cnconst2  15334  cnpdis  15343  txdis  15378  txdis1cn  15379  fsumcncntop  15668  dvef  15828  plyf  15838  elplyr  15841  elplyd  15842  ply1term  15844  plyaddlem  15850  plymullem  15851  plycolemc  15859  plycn  15863  dvply2g  15867  perfectlem2  16114  upgr1elem1  16361  bj-omtrans  16982  pwtrufal  17027