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

Theorem ssini 4223
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 470 . 2 (𝐴𝐵𝐴𝐶)
4 ssin 4222 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4mpbi 229 1 𝐴 ⊆ (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 395  cin 3939  wss 3940
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 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957
This theorem is referenced by:  inv1  4386  cnvrescnv  6184  hartogslem1  9533  xptrrel  14924  fbasrn  23710  limciun  25745  hlimcaui  30958  chdmm1i  31199  chm0i  31212  ledii  31258  lejdii  31260  mayetes3i  31451  mdslj2i  32042  mdslmd2i  32052  sumdmdlem2  32141  sigapildsys  33649  ssoninhaus  35823  bj-disj2r  36399  bj-idres  36531  bj-rvecsscvec  36675  icomnfinre  44750  fouriersw  45432  sge0split  45610
  Copyright terms: Public domain W3C validator