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

Theorem coss1 5812
Description: Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
Assertion
Ref Expression
coss1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))

Proof of Theorem coss1
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssbr 5150 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑧𝑦𝐵𝑧))
21anim2d 613 . . . 4 (𝐴𝐵 → ((𝑥𝐶𝑦𝑦𝐴𝑧) → (𝑥𝐶𝑦𝑦𝐵𝑧)))
32eximdv 1921 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)))
43ssopab2dv 5509 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)})
5 df-co 5643 . 2 (𝐴𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)}
6 df-co 5643 . 2 (𝐵𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)}
74, 5, 63sstr4g 3990 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782  wss 3911   class class class wbr 5106  {copab 5168  ccom 5638
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-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-co 5643
This theorem is referenced by:  coeq1  5814  funss  6521  tposss  8159  cottrcl  9660  frmin  9690  frrlem16  9699  rtrclreclem4  14952  tsrdir  18498  ustex2sym  23584  ustex3sym  23585  ustneism  23591  trust  23597  utop2nei  23618  neipcfilu  23664  trclubgNEW  41978  trrelsuperrel2dg  42031  trclrelexplem  42071  cotrcltrcl  42085  cotrclrcl  42102  frege96d  42109  frege97d  42112  frege109d  42117  frege131d  42124
  Copyright terms: Public domain W3C validator