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

Theorem coss1 5615
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 5008 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑧𝑦𝐵𝑧))
21anim2d 611 . . . 4 (𝐴𝐵 → ((𝑥𝐶𝑦𝑦𝐴𝑧) → (𝑥𝐶𝑦𝑦𝐵𝑧)))
32eximdv 1896 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)))
43ssopab2dv 5329 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)})
5 df-co 5455 . 2 (𝐴𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)}
6 df-co 5455 . 2 (𝐵𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)}
74, 5, 63sstr4g 3935 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1762  wss 3861   class class class wbr 4964  {copab 5026  ccom 5450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-in 3868  df-ss 3876  df-br 4965  df-opab 5027  df-co 5455
This theorem is referenced by:  coeq1  5617  funss  6247  tposss  7747  rtrclreclem4  14254  tsrdir  17677  ustex2sym  22508  ustex3sym  22509  ustneism  22515  trust  22521  utop2nei  22542  neipcfilu  22588  trclubgNEW  39476  trrelsuperrel2dg  39514  trclrelexplem  39554  cotrcltrcl  39568  cotrclrcl  39585  frege96d  39592  frege97d  39595  frege109d  39600  frege131d  39607
  Copyright terms: Public domain W3C validator