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

Theorem ssdifss 4096
Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
Assertion
Ref Expression
ssdifss (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)

Proof of Theorem ssdifss
StepHypRef Expression
1 difss 4092 . 2 (𝐴𝐶) ⊆ 𝐴
2 sstr 3953 . 2 (((𝐴𝐶) ⊆ 𝐴𝐴𝐵) → (𝐴𝐶) ⊆ 𝐵)
31, 2mpan 689 1 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3908  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928
This theorem is referenced by:  ssdifssd  4103  xrsupss  13234  xrinfmss  13235  rpnnen2lem12  16112  lpval  22506  lpdifsn  22510  islp2  22512  lpcls  22731  mblfinlem3  36163  mblfinlem4  36164  voliunnfl  36168  ssdifcl  41931  sssymdifcl  41932  supxrmnf2  43754  infxrpnf2  43784  fourierdlem102  44535  fourierdlem114  44547  lindslinindimp2lem4  46628  lindslinindsimp2lem5  46629  lindslinindsimp2  46630  lincresunit3  46648
  Copyright terms: Public domain W3C validator