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

Theorem ssres2 6005
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 5682 . . 3 (𝐴𝐵 → (𝐴 × V) ⊆ (𝐵 × V))
2 sslin 4195 . . 3 ((𝐴 × V) ⊆ (𝐵 × V) → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
31, 2syl 18 . 2 (𝐴𝐵 → (𝐶 ∩ (𝐴 × V)) ⊆ (𝐶 ∩ (𝐵 × V)))
4 df-res 5675 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
5 df-res 5675 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
63, 4, 53sstr4g 3991 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  Vcvv 3457  cin 3905  wss 3906   × cxp 5661  cres 5665
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-opab 5176  df-xp 5669  df-res 5675
This theorem is used by:  imass2  6106  imadifssran  6204  1stcof  8022  2ndcof  8023  tfrlem15  8385  gsum2dlem2  20087  txkgen  23862  funpsstri  36297  eldisjss  39547  resnonrel  44378  mptrcllem  44399  rtrclexi  44407  cnvrcl0  44411  relexpss1d  44491  relexp0a  44502  supcnvlimsup  46514
  Copyright terms: Public domain W3C validator