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

Theorem coss2 5857
Description: Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
Assertion
Ref Expression
coss2 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))

Proof of Theorem coss2
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssbr 5193 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑦𝑥𝐵𝑦))
21anim1d 609 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝑦𝐶𝑧) → (𝑥𝐵𝑦𝑦𝐶𝑧)))
32eximdv 1918 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)))
43ssopab2dv 5552 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)})
5 df-co 5686 . 2 (𝐶𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)}
6 df-co 5686 . 2 (𝐶𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)}
74, 5, 63sstr4g 4028 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wex 1779  wss 3949   class class class wbr 5149  {copab 5211  ccom 5681
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686
This theorem is referenced by:  coeq2  5859  funss  6568  tposss  8216  dftpos4  8234  ttrclco  9717  frmin  9748  frrlem16  9757  rtrclreclem4  15014  tsrdir  18563  mvdco  19356  ustex2sym  23943  ustex3sym  23944  ustneism  23950  trust  23956  utop2nei  23977  neipcfilu  24023  fcoinver  32100  trclubgNEW  42673  trrelsuperrel2dg  42726
  Copyright terms: Public domain W3C validator