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

Theorem ssrin 4160
 Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
ssrin (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))

Proof of Theorem ssrin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ssel 3908 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 613 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elin 3897 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elin 3897 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 299 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3921 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   ∩ cin 3880   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  sslin  4161  ssrind  4162  ss2in  4163  ssdisj  4367  ssdifin0  4389  ssres  5846  predpredss  6123  sbthlem7  8620  onsdominel  8653  phplem2  8684  infdifsn  9107  fin23lem23  9740  ttukeylem2  9924  limsupgord  14824  pjfval  20400  pjpm  20402  tgss  21583  neindisj2  21738  1stcrest  22068  kgencn3  22173  trfbas2  22458  fclsrest  22639  fcfnei  22650  cnextcn  22682  tsmsres  22759  trust  22845  restutopopn  22854  metrest  23141  reperflem  23433  ellimc3  24492  limcflf  24494  lhop1lem  24626  ppinprm  25747  chtnprm  25749  chtppilimlem1  26067  orthin  29239  3oalem6  29460  mdslle1i  30110  mdslle2i  30111  mdslj1i  30112  mdslj2i  30113  mdslmd1lem2  30119  mdslmd3i  30125  mdexchi  30128  eulerpartlemn  31764  poimirlem3  35079  poimirlem29  35105  ismblfin  35117  nnuzdisj  42030  sumnnodd  42315  liminfgord  42439  sge0less  43074
 Copyright terms: Public domain W3C validator