Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssind Structured version   Visualization version   GIF version

Theorem ssind 4183
 Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
ssind.1 (𝜑𝐴𝐵)
ssind.2 (𝜑𝐴𝐶)
Assertion
Ref Expression
ssind (𝜑𝐴 ⊆ (𝐵𝐶))

Proof of Theorem ssind
StepHypRef Expression
1 ssind.1 . . 3 (𝜑𝐴𝐵)
2 ssind.2 . . 3 (𝜑𝐴𝐶)
31, 2jca 515 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
4 ssin 4181 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4sylib 221 1 (𝜑𝐴 ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3907   ⊆ wss 3908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925 This theorem is referenced by:  mreexexlem3d  16908  isacs1i  16919  rescabs  17094  funcres2c  17162  lsmmod  18792  gsumzres  19020  gsumzsubmcl  19029  gsum2d  19083  issubdrg  19551  lspdisj  19888  mplind  20739  ntrin  21664  elcls  21676  neitr  21783  restcls  21784  lmss  21901  xkoinjcn  22290  trfg  22494  trust  22833  utoptop  22838  restutop  22841  isngp2  23201  lebnumii  23569  causs  23900  dvreslem  24510  c1lip3  24600  ssjo  29228  dmdbr5  30089  mdslj2i  30101  mdsl2bi  30104  mdslmd1lem2  30107  mdsymlem5  30188  difininv  30286  idlsrgmulrssin  31037  bnj1286  32365  mclsind  32891  frrlem12  33208  frrlem13  33209  neiin  33754  topmeet  33786  fnemeet2  33789  bj-elpwg  34430  bj-restpw  34468  bj-restb  34470  bj-restuni2  34474  idresssidinxp  35684  pmod1i  37102  dihmeetlem1N  38544  dihglblem5apreN  38545  dochdmj1  38644  mapdin  38916  baerlem3lem2  38964  baerlem5alem2  38965  baerlem5blem2  38966  trrelind  40296  isotone2  40685  nzin  40956  inmap  41776  islptre  42200  limccog  42201  limcresiooub  42223  limcresioolb  42224  limsupresxr  42347  liminfresxr  42348  liminfvalxr  42364  fourierdlem48  42735  fourierdlem49  42736  fourierdlem113  42800  pimiooltgt  43285  pimdecfgtioc  43289  pimincfltioc  43290  pimdecfgtioo  43291  pimincfltioo  43292  sssmf  43311  smflimlem2  43344  smfsuplem1  43381  setrec2fun  45161
 Copyright terms: Public domain W3C validator