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

Theorem coss1 5861
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 5196 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑧𝑦𝐵𝑧))
21anim2d 610 . . . 4 (𝐴𝐵 → ((𝑥𝐶𝑦𝑦𝐴𝑧) → (𝑥𝐶𝑦𝑦𝐵𝑧)))
32eximdv 1912 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)))
43ssopab2dv 5556 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)})
5 df-co 5690 . 2 (𝐴𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)}
6 df-co 5690 . 2 (𝐵𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)}
74, 5, 63sstr4g 4024 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wex 1773  wss 3946   class class class wbr 5152  {copab 5214  ccom 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3963  df-br 5153  df-opab 5215  df-co 5690
This theorem is referenced by:  coeq1  5863  funss  6577  tposss  8241  cottrcl  9758  frmin  9788  frrlem16  9797  rtrclreclem4  15061  tsrdir  18624  ustex2sym  24204  ustex3sym  24205  ustneism  24211  trust  24217  utop2nei  24238  neipcfilu  24284  trclubgNEW  43222  trrelsuperrel2dg  43275  trclrelexplem  43315  cotrcltrcl  43329  cotrclrcl  43346  frege96d  43353  frege97d  43356  frege109d  43361  frege131d  43368
  Copyright terms: Public domain W3C validator