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

Theorem ssini 4210
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 473 . 2 (𝐴𝐵𝐴𝐶)
4 ssin 4209 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4mpbi 232 1 𝐴 ⊆ (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 398  cin 3937  wss 3938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954
This theorem is referenced by:  inv1  4350  cnvrescnv  6054  hartogslem1  9008  xptrrel  14342  fbasrn  22494  limciun  24494  hlimcaui  29015  chdmm1i  29256  chm0i  29269  ledii  29315  lejdii  29317  mayetes3i  29508  mdslj2i  30099  mdslmd2i  30109  sumdmdlem2  30198  sigapildsys  31423  ssoninhaus  33798  bj-disj2r  34342  bj-idres  34454  bj-rvecsscvec  34587  icomnfinre  41835  fouriersw  42523  sge0split  42698
  Copyright terms: Public domain W3C validator