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