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

Theorem ssrin 4242
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 3977 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 611 . . 3 (𝐴𝐵 → ((𝑥𝐴𝑥𝐶) → (𝑥𝐵𝑥𝐶)))
3 elin 3967 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elin 3967 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43imtr4g 296 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3989 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  cin 3950  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968
This theorem is referenced by:  sslin  4243  ssrind  4244  ss2in  4245  ssdisj  4460  ssdifin0  4486  ssres  6021  predpredss  6328  sbthlem7  9129  onsdominel  9166  phplem2OLD  9255  infdifsn  9697  fin23lem23  10366  ttukeylem2  10550  limsupgord  15508  pjfval  21726  pjpm  21728  tgss  22975  neindisj2  23131  1stcrest  23461  kgencn3  23566  trfbas2  23851  fclsrest  24032  fcfnei  24043  cnextcn  24075  tsmsres  24152  trust  24238  restutopopn  24247  metrest  24537  reperflem  24840  ellimc3  25914  limcflf  25916  lhop1lem  26052  ppinprm  27195  chtnprm  27197  chtppilimlem1  27517  orthin  31465  3oalem6  31686  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mdslmd1lem2  32345  mdslmd3i  32351  mdexchi  32354  eulerpartlemn  34383  poimirlem3  37630  poimirlem29  37656  ismblfin  37668  nnuzdisj  45366  sumnnodd  45645  liminfgord  45769  sge0less  46407  sepnsepo  48821
  Copyright terms: Public domain W3C validator