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

Theorem ssind 3525
Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
ssind.1  |-  ( ph  ->  A  C_  B )
ssind.2  |-  ( ph  ->  A  C_  C )
Assertion
Ref Expression
ssind  |-  ( ph  ->  A  C_  ( B  i^i  C ) )

Proof of Theorem ssind
StepHypRef Expression
1 ssind.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssind.2 . 2  |-  ( ph  ->  A  C_  C )
3 ssin 3523 . . 3  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
43biimpi 187 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  ->  A  C_  ( B  i^i  C ) )
51, 2, 4syl2anc 643 1  |-  ( ph  ->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    i^i cin 3279    C_ wss 3280
This theorem is referenced by:  mreexexlem3d  13826  isacs1i  13837  rescabs  13988  funcres2c  14053  lsmmod  15262  gsumzres  15472  gsumzsubmcl  15478  gsum2d  15501  issubdrg  15848  lspdisj  16152  mplind  16517  ntrin  17080  elcls  17092  neitr  17198  restcls  17199  lmss  17316  xkoinjcn  17672  trfg  17876  trust  18212  utoptop  18217  restutop  18220  isngp2  18597  lebnumii  18944  causs  19204  dvreslem  19749  c1lip3  19836  ssjo  22902  dmdbr5  23764  mdslj2i  23776  mdsl2bi  23779  mdslmd1lem2  23782  mdsymlem5  23863  neiin  26225  topmeet  26283  fnemeet2  26286  bnj1286  29094  pmod1i  30330  dihmeetlem1N  31773  dihglblem5apreN  31774  dochdmj1  31873  mapdin  32145  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator