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  7549  pw1m  7584  un0addcl  9601  un0mulcl  9602  fseq1p1m1  10512  hashfibclem  11298  hashf1lem1  11301  hashf1lem2  11302  fsumge1  12247  fprodsplit1f  12420  bitsinv1  12748  phicl2  13015  ennnfonelemhf1o  13356  imasaddfnlemg  13688  imasaddflemg  13690  0subm  13844  gsumvallem2  13853  trivsubgd  14056  trivsubgsnd  14057  trivnsgd  14073  kerf1ghm  14130  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  lsssn0  14791  lss0ss  14792  lsptpcl  14815  lspsnvsi  14839  lspun0  14846  mulgrhm2  15029  zndvds  15068  rest0  15371  iscnp4  15410  cnconst2  15425  cnpdis  15434  txdis  15469  txdis1cn  15470  fsumcncntop  15759  dvef  15919  plyf  15929  elplyr  15932  elplyd  15933  ply1term  15935  plyaddlem  15941  plymullem  15942  plycolemc  15950  plycn  15954  dvply2g  15958  ppiprm  16220  chtprm  16222  perfectlem2  16261  upgr1elem1  16527  bj-omtrans  17148  pwtrufal  17193