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

Theorem ssres2 6002
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 5679 . . 3 (𝐴𝐵 → (𝐴 × V) ⊆ (𝐵 × V))
2 sslin 4194 . . 3 ((𝐴 × V) ⊆ (𝐵 × V) → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
31, 2syl 18 . 2 (𝐴𝐵 → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
4 df-res 5672 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
5 df-res 5672 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
63, 4, 53sstr4g 3989 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  Vcvv 3454  cin 3903  wss 3904   × cxp 5658  cres 5662
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734
This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-opab 5173  df-xp 5666  df-res 5672
This theorem is used by:  imass2  6103  imadifssran  6201  1stcof  8014  2ndcof  8015  tfrlem15  8377  gsum2dlem2  20047  txkgen  23820  funpsstri  36266  eldisjss  39515  resnonrel  44346  mptrcllem  44367  rtrclexi  44375  cnvrcl0  44379  relexpss1d  44459  relexp0a  44470  supcnvlimsup  46482
  Copyright terms: Public domain W3C validator