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

Theorem ssind 3870
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 553 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
4 ssin 3868 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4sylib 208 1 (𝜑𝐴 ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  cin 3606  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621
This theorem is referenced by:  mreexexlem3d  16353  isacs1i  16365  rescabs  16540  funcres2c  16608  lsmmod  18134  gsumzres  18356  gsumzsubmcl  18364  gsum2d  18417  issubdrg  18853  lspdisj  19173  mplind  19550  ntrin  20913  elcls  20925  neitr  21032  restcls  21033  lmss  21150  xkoinjcn  21538  trfg  21742  trust  22080  utoptop  22085  restutop  22088  isngp2  22448  lebnumii  22812  causs  23142  dvreslem  23718  c1lip3  23807  ssjo  28434  dmdbr5  29295  mdslj2i  29307  mdsl2bi  29310  mdslmd1lem2  29313  mdsymlem5  29394  difininv  29480  bnj1286  31213  mclsind  31593  neiin  32452  topmeet  32484  fnemeet2  32487  bj-restpw  33170  bj-restb  33172  bj-restuni2  33176  idresssidinxp  34220  pmod1i  35452  dihmeetlem1N  36896  dihglblem5apreN  36897  dochdmj1  36996  mapdin  37268  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  trrelind  38274  isotone2  38664  nzin  38834  inmap  39715  islptre  40169  limccog  40170  limcresiooub  40192  limcresioolb  40193  limsupresxr  40316  liminfresxr  40317  liminfvalxr  40333  fourierdlem48  40689  fourierdlem49  40690  fourierdlem113  40754  pimiooltgt  41242  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  sssmf  41268  smflimlem2  41301  smfsuplem1  41338  setrec2fun  42764
  Copyright terms: Public domain W3C validator