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

Theorem ssdifss 3884
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 3880 . 2 (𝐴𝐶) ⊆ 𝐴
2 sstr 3752 . 2 (((𝐴𝐶) ⊆ 𝐴𝐴𝐵) → (𝐴𝐶) ⊆ 𝐵)
31, 2mpan 708 1 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3712  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729
This theorem is referenced by:  ssdifssd  3891  xrsupss  12352  xrinfmss  12353  rpnnen2lem12  15173  lpval  21165  lpdifsn  21169  islp2  21171  lpcls  21390  mblfinlem3  33779  mblfinlem4  33780  voliunnfl  33784  ssdifcl  38396  sssymdifcl  38397  supxrmnf2  40176  infxrpnf2  40209  fourierdlem102  40946  fourierdlem114  40958  lindslinindimp2lem4  42778  lindslinindsimp2lem5  42779  lindslinindsimp2  42780  lincresunit3  42798
  Copyright terms: Public domain W3C validator