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

Theorem coss2 5714
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 5096 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑦𝑥𝐵𝑦))
21anim1d 613 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝑦𝐶𝑧) → (𝑥𝐵𝑦𝑦𝐶𝑧)))
32eximdv 1919 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)))
43ssopab2dv 5425 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)})
5 df-co 5551 . 2 (𝐶𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)}
6 df-co 5551 . 2 (𝐶𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)}
74, 5, 63sstr4g 3998 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wex 1781  wss 3919   class class class wbr 5052  {copab 5114  ccom 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-in 3926  df-ss 3936  df-br 5053  df-opab 5115  df-co 5551
This theorem is referenced by:  coeq2  5716  funss  6362  tposss  7889  dftpos4  7907  rtrclreclem4  14420  tsrdir  17848  mvdco  18573  ustex2sym  22828  ustex3sym  22829  ustneism  22835  trust  22841  utop2nei  22862  neipcfilu  22908  fcoinver  30371  trclubgNEW  40238  trrelsuperrel2dg  40292
  Copyright terms: Public domain W3C validator