Theorem snssi 3776

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

Syntax hints:   → wi 4   ∈ wcel 2175   ⊆ wss 3165  {csn 3632

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-in 3171  df-ss 3178  df-sn 3638

This theorem is referenced by:  difsnss  3778  sssnm  3794  tpssi  3799  snelpwi  4255  intid  4267  abnexg  4492  ordsucss  4551  xpsspw  4786  djussxp  4822  xpimasn  5130  fconst6g  5473  f1sng  5563  fvimacnvi  5693  fsn2  5753  fnressn  5769  fsnunf  5783  mapsn  6776  unsnfidcel  7017  en1eqsn  7049  exmidfodomrlemim  7308  axresscn  7972  nn0ssre  9298  1fv  10260  fxnn0nninf  10582  1exp  10711  hashdifsn  10962  hashdifpr  10963  fsum00  11744  hash2iun1dif1  11762  4sqlem19  12703  exmidunben  12768  lspsncl  14125  lspsnss  14137  lspsnid  14140  znlidl  14367  isneip  14589  neipsm  14597  opnneip  14602  plyun0  15179  plycjlemc  15203  plycj  15204  plyrecj  15206  dvply2g  15209  perfectlem2  15443