ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  snssi GIF version

Theorem snssi 3735
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
StepHypRef Expression
1 snssg 3725 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
21ibi 176 1 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wss 3129  {csn 3591
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135  df-ss 3142  df-sn 3597
This theorem is referenced by:  difsnss  3737  sssnm  3752  tpssi  3757  snelpwi  4209  intid  4221  abnexg  4443  ordsucss  4500  xpsspw  4735  djussxp  4768  xpimasn  5073  fconst6g  5410  f1sng  5499  fvimacnvi  5626  fsn2  5686  fnressn  5698  fsnunf  5712  mapsn  6684  unsnfidcel  6914  en1eqsn  6941  exmidfodomrlemim  7194  axresscn  7847  nn0ssre  9166  1fv  10122  fxnn0nninf  10421  1exp  10532  hashdifsn  10780  hashdifpr  10781  fsum00  11451  hash2iun1dif1  11469  exmidunben  12407  isneip  13306  neipsm  13314  opnneip  13319
  Copyright terms: Public domain W3C validator