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

Theorem ssind 4231
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 510 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
4 ssin 4229 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4sylib 217 1 (𝜑𝐴 ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  cin 3943  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-in 3951  df-ss 3961
This theorem is referenced by:  frrlem12  8303  frrlem13  8304  mreexexlem3d  17629  isacs1i  17640  rescabs  17821  rescabsOLD  17822  funcres2c  17893  lsmmod  19642  gsumzres  19876  gsumzsubmcl  19885  gsum2d  19939  issubdrg  20680  lspdisj  21025  mplind  22036  ntrin  23009  elcls  23021  neitr  23128  restcls  23129  lmss  23246  xkoinjcn  23635  trfg  23839  trust  24178  utoptop  24183  restutop  24186  isngp2  24550  lebnumii  24936  causs  25270  dvreslem  25882  c1lip3  25976  ssjo  31329  dmdbr5  32190  mdslj2i  32202  mdsl2bi  32205  mdslmd1lem2  32208  mdsymlem5  32289  difininv  32392  idlsrgmulrssin  33325  bnj1286  34781  mclsind  35311  neiin  35947  topmeet  35979  fnemeet2  35982  bj-elpwg  36662  bj-restpw  36702  bj-restb  36704  bj-restuni2  36708  idresssidinxp  37910  pmod1i  39451  dihmeetlem1N  40893  dihglblem5apreN  40894  dochdmj1  40993  mapdin  41265  baerlem3lem2  41313  baerlem5alem2  41314  baerlem5blem2  41315  trrelind  43237  isotone2  43621  nzin  43897  inmap  44721  islptre  45145  limccog  45146  limcresiooub  45168  limcresioolb  45169  limsupresxr  45292  liminfresxr  45293  liminfvalxr  45309  fourierdlem48  45680  fourierdlem49  45681  fourierdlem113  45745  pimiooltgt  46236  pimdecfgtioc  46241  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  sssmf  46264  smflimlem2  46298  smfsuplem1  46337  iscnrm3llem2  48155  setrec2fun  48309
  Copyright terms: Public domain W3C validator