Theorem snssi 3777

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 3767	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 176	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2176   ⊆ wss 3166  {csn 3633

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-sn 3639

This theorem is referenced by:  difsnss  3779  sssnm  3795  tpssi  3800  snelpwi  4256  intid  4268  abnexg  4493  ordsucss  4552  xpsspw  4787  djussxp  4823  xpimasn  5131  fconst6g  5474  f1sng  5564  fvimacnvi  5694  fsn2  5754  fnressn  5770  fsnunf  5784  mapsn  6777  unsnfidcel  7018  en1eqsn  7050  exmidfodomrlemim  7309  axresscn  7973  nn0ssre  9299  1fv  10261  fxnn0nninf  10584  1exp  10713  hashdifsn  10964  hashdifpr  10965  fsum00  11773  hash2iun1dif1  11791  4sqlem19  12732  exmidunben  12797  lspsncl  14154  lspsnss  14166  lspsnid  14169  znlidl  14396  isneip  14618  neipsm  14626  opnneip  14631  plyun0  15208  plycjlemc  15232  plycj  15233  plyrecj  15235  dvply2g  15238  perfectlem2  15472