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

Theorem snssd 3777
Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
snssd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
snssd (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2 (𝜑𝐴𝐵)
2 snssg 3766 . . 3 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
31, 2syl 14 . 2 (𝜑 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
41, 3mpbid 147 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  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:  pwntru  4242  ecinxp  6696  xpdom3m  6928  ac6sfi  6994  undifdc  7020  iunfidisj  7047  fidcenumlemr  7056  ssfii  7075  en2other2  7303  un0addcl  9327  un0mulcl  9328  fseq1p1m1  10215  fsumge1  11714  fprodsplit1f  11887  bitsinv1  12215  phicl2  12478  ennnfonelemhf1o  12726  imasaddfnlemg  13088  imasaddflemg  13090  0subm  13258  gsumvallem2  13267  trivsubgd  13478  trivsubgsnd  13479  trivnsgd  13495  kerf1ghm  13552  lsssn0  14074  lss0ss  14075  lsptpcl  14098  lspsnvsi  14122  lspun0  14129  mulgrhm2  14314  zndvds  14353  rest0  14593  iscnp4  14632  cnconst2  14647  cnpdis  14656  txdis  14691  txdis1cn  14692  fsumcncntop  14981  dvef  15141  plyf  15151  elplyr  15154  elplyd  15155  ply1term  15157  plyaddlem  15163  plymullem  15164  plycolemc  15172  plycn  15176  dvply2g  15180  perfectlem2  15414  bj-omtrans  15825  pwtrufal  15867
  Copyright terms: Public domain W3C validator