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

Theorem ssini 4165
Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
Hypotheses
Ref Expression
ssini.1 𝐴𝐵
ssini.2 𝐴𝐶
Assertion
Ref Expression
ssini 𝐴 ⊆ (𝐵𝐶)

Proof of Theorem ssini
StepHypRef Expression
1 ssini.1 . . 3 𝐴𝐵
2 ssini.2 . . 3 𝐴𝐶
31, 2pm3.2i 471 . 2 (𝐴𝐵𝐴𝐶)
4 ssin 4164 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4mpbi 229 1 𝐴 ⊆ (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 396  cin 3886  wss 3887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904
This theorem is referenced by:  inv1  4328  cnvrescnv  6098  hartogslem1  9301  xptrrel  14691  fbasrn  23035  limciun  25058  hlimcaui  29598  chdmm1i  29839  chm0i  29852  ledii  29898  lejdii  29900  mayetes3i  30091  mdslj2i  30682  mdslmd2i  30692  sumdmdlem2  30781  sigapildsys  32130  ssoninhaus  34637  bj-disj2r  35218  bj-idres  35331  bj-rvecsscvec  35475  icomnfinre  43090  fouriersw  43772  sge0split  43947
  Copyright terms: Public domain W3C validator