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

Theorem ssini 4056
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 464 . 2 (𝐴𝐵𝐴𝐶)
4 ssin 4055 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4mpbi 222 1 𝐴 ⊆ (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 386  cin 3791  wss 3792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806
This theorem is referenced by:  inv1  4196  hartogslem1  8738  xptrrel  14134  fbasrn  22107  limciun  24106  hlimcaui  28682  chdmm1i  28925  chm0i  28938  ledii  28984  lejdii  28986  mayetes3i  29177  mdslj2i  29768  mdslmd2i  29778  sumdmdlem2  29867  sigapildsys  30831  ssoninhaus  33038  bj-disj2r  33593  icomnfinre  40701  fouriersw  41389  sge0split  41564
  Copyright terms: Public domain W3C validator