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

Theorem ssres2 6010
Description: Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
ssres2 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))

Proof of Theorem ssres2
StepHypRef Expression
1 xpss1 5696 . . 3 (𝐴𝐵 → (𝐴 × V) ⊆ (𝐵 × V))
2 sslin 4235 . . 3 ((𝐴 × V) ⊆ (𝐵 × V) → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
31, 2syl 17 . 2 (𝐴𝐵 → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
4 df-res 5689 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
5 df-res 5689 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
63, 4, 53sstr4g 4028 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  Vcvv 3475  cin 3948  wss 3949   × cxp 5675  cres 5679
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-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-res 5689
This theorem is referenced by:  imass2  6102  1stcof  8005  2ndcof  8006  tfrlem15  8392  gsum2dlem2  19839  txkgen  23156  funpsstri  34737  eldisjss  37608  resnonrel  42343  mptrcllem  42364  rtrclexi  42372  cnvrcl0  42376  relexpss1d  42456  relexp0a  42467  supcnvlimsup  44456
  Copyright terms: Public domain W3C validator