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

Theorem coss1 5199
 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 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
21ssbrd 4626 . . . . 5 (𝐴𝐵 → (𝑦𝐴𝑧𝑦𝐵𝑧))
32anim2d 587 . . . 4 (𝐴𝐵 → ((𝑥𝐶𝑦𝑦𝐴𝑧) → (𝑥𝐶𝑦𝑦𝐵𝑧)))
43eximdv 1833 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)))
54ssopab2dv 4929 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)})
6 df-co 5047 . 2 (𝐴𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐴𝑧)}
7 df-co 5047 . 2 (𝐵𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦𝑦𝐵𝑧)}
85, 6, 73sstr4g 3609 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ⊆ wss 3540   class class class wbr 4583  {copab 4642   ∘ ccom 5042 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047 This theorem is referenced by:  coeq1  5201  funss  5822  tposss  7240  rtrclreclem4  13649  tsrdir  17061  ustex2sym  21830  ustex3sym  21831  ustund  21835  ustneism  21837  trust  21843  utop2nei  21864  neipcfilu  21910  trclubgNEW  36944  trrelsuperrel2dg  36982  trclrelexplem  37022  cotrcltrcl  37036  cotrclrcl  37053  frege96d  37060  frege97d  37063  frege109d  37068  frege131d  37075
 Copyright terms: Public domain W3C validator