Theorem snssi 3766

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

Syntax hints:   → wi 4   ∈ wcel 2167   ⊆ wss 3157  {csn 3622

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 3628

This theorem is referenced by:  difsnss  3768  sssnm  3784  tpssi  3789  snelpwi  4245  intid  4257  abnexg  4481  ordsucss  4540  xpsspw  4775  djussxp  4811  xpimasn  5118  fconst6g  5456  f1sng  5546  fvimacnvi  5676  fsn2  5736  fnressn  5748  fsnunf  5762  mapsn  6749  unsnfidcel  6982  en1eqsn  7014  exmidfodomrlemim  7268  axresscn  7927  nn0ssre  9253  1fv  10214  fxnn0nninf  10531  1exp  10660  hashdifsn  10911  hashdifpr  10912  fsum00  11627  hash2iun1dif1  11645  4sqlem19  12578  exmidunben  12643  lspsncl  13948  lspsnss  13960  lspsnid  13963  znlidl  14190  isneip  14382  neipsm  14390  opnneip  14395  plyun0  14972  plycjlemc  14996  plycj  14997  plyrecj  14999  dvply2g  15002  perfectlem2  15236