Theorem snssi 3767

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
snssi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 3757	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 176	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ 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:  difsnss  3769  sssnm  3785  tpssi  3790  snelpwi  4246  intid  4258  abnexg  4482  ordsucss  4541  xpsspw  4776  djussxp  4812  xpimasn  5119  fconst6g  5459  f1sng  5549  fvimacnvi  5679  fsn2  5739  fnressn  5751  fsnunf  5765  mapsn  6758  unsnfidcel  6991  en1eqsn  7023  exmidfodomrlemim  7282  axresscn  7946  nn0ssre  9272  1fv  10233  fxnn0nninf  10550  1exp  10679  hashdifsn  10930  hashdifpr  10931  fsum00  11646  hash2iun1dif1  11664  4sqlem19  12605  exmidunben  12670  lspsncl  14026  lspsnss  14038  lspsnid  14041  znlidl  14268  isneip  14490  neipsm  14498  opnneip  14503  plyun0  15080  plycjlemc  15104  plycj  15105  plyrecj  15107  dvply2g  15110  perfectlem2  15344