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

Theorem coss1 5724
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 5097 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑧𝑦𝐵𝑧))
21anim2d 615 . . . 4 (𝐴𝐵 → ((𝑥𝐶𝑦𝑦𝐴𝑧) → (𝑥𝐶𝑦𝑦𝐵𝑧)))
32eximdv 1925 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)))
43ssopab2dv 5432 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)})
5 df-co 5560 . 2 (𝐴𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)}
6 df-co 5560 . 2 (𝐵𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)}
74, 5, 63sstr4g 3946 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wex 1787  wss 3866   class class class wbr 5053  {copab 5115  ccom 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-br 5054  df-opab 5116  df-co 5560
This theorem is referenced by:  coeq1  5726  funss  6399  tposss  7969  rtrclreclem4  14624  tsrdir  18110  ustex2sym  23114  ustex3sym  23115  ustneism  23121  trust  23127  utop2nei  23148  neipcfilu  23193  cottrcl  33518  trclubgNEW  40902  trrelsuperrel2dg  40956  trclrelexplem  40996  cotrcltrcl  41010  cotrclrcl  41027  frege96d  41034  frege97d  41037  frege109d  41042  frege131d  41049
  Copyright terms: Public domain W3C validator