Theorem snssi 3812

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

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3197  {csn 3666

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210  df-sn 3672

This theorem is referenced by:  difsnss  3814  sssnm  3832  tpssi  3837  snelpwi  4297  intid  4310  abnexg  4537  ordsucss  4596  xpsspw  4831  djussxp  4867  xpimasn  5177  fconst6g  5526  f1sng  5617  fvimacnvi  5751  fsn2  5811  fnressn  5829  fsnunf  5843  mapsn  6845  unsnfidcel  7094  en1eqsn  7126  exmidfodomrlemim  7390  axresscn  8058  nn0ssre  9384  1fv  10347  fxnn0nninf  10673  1exp  10802  hashdifsn  11054  hashdifpr  11055  fsum00  11988  hash2iun1dif1  12006  4sqlem19  12947  exmidunben  13012  lspsncl  14371  lspsnss  14383  lspsnid  14386  znlidl  14613  isneip  14835  neipsm  14843  opnneip  14848  plyun0  15425  plycjlemc  15449  plycj  15450  plyrecj  15452  dvply2g  15455  perfectlem2  15689