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

Theorem ssini 3707
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  |-  A  C_  B
ssini.2  |-  A  C_  C
Assertion
Ref Expression
ssini  |-  A  C_  ( B  i^i  C )

Proof of Theorem ssini
StepHypRef Expression
1 ssini.1 . . 3  |-  A  C_  B
2 ssini.2 . . 3  |-  A  C_  C
31, 2pm3.2i 453 . 2  |-  ( A 
C_  B  /\  A  C_  C )
4 ssin 3706 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
53, 4mpbi 208 1  |-  A  C_  ( B  i^i  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    i^i cin 3460    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475
This theorem is referenced by:  inv1  3811  hartogslem1  7959  xptrrel  12898  fbasrn  20551  limciun  22464  hlimcaui  26352  chdmm1i  26593  chm0i  26606  ledii  26652  lejdii  26654  mayetes3i  26846  mdslj2i  27437  mdslmd2i  27447  sumdmdlem2  27536  sigapildsys  28388  ssoninhaus  30141  fouriersw  32253
  Copyright terms: Public domain W3C validator