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

Theorem ssdifss 3703
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 3699 . 2 (𝐴𝐶) ⊆ 𝐴
2 sstr 3576 . 2 (((𝐴𝐶) ⊆ 𝐴𝐴𝐵) → (𝐴𝐶) ⊆ 𝐵)
31, 2mpan 702 1 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3537  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554
This theorem is referenced by:  ssdifssd  3710  xrsupss  12011  xrinfmss  12012  rpnnen2lem12  14793  lpval  20753  lpdifsn  20757  islp2  20759  lpcls  20978  mblfinlem3  32618  mblfinlem4  32619  voliunnfl  32623  ssdifcl  36895  sssymdifcl  36896  fourierdlem102  39101  fourierdlem114  39113  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lincresunit3  42064
  Copyright terms: Public domain W3C validator