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

Theorem coss2 5478
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 4886 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑦𝑥𝐵𝑦))
21anim1d 600 . . . 4 (𝐴𝐵 → ((𝑥𝐴𝑦𝑦𝐶𝑧) → (𝑥𝐵𝑦𝑦𝐶𝑧)))
32eximdv 2008 . . 3 (𝐴𝐵 → (∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)))
43ssopab2dv 5197 . 2 (𝐴𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)})
5 df-co 5318 . 2 (𝐶𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦𝑦𝐶𝑧)}
6 df-co 5318 . 2 (𝐶𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦𝑦𝐶𝑧)}
74, 5, 63sstr4g 3841 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wex 1859  wss 3767   class class class wbr 4842  {copab 4904  ccom 5313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-in 3774  df-ss 3781  df-br 4843  df-opab 4905  df-co 5318
This theorem is referenced by:  coeq2  5480  funss  6118  tposss  7586  dftpos4  7604  rtrclreclem4  14022  tsrdir  17441  mvdco  18064  ustex2sym  22231  ustex3sym  22232  ustund  22236  ustneism  22238  trust  22244  utop2nei  22265  neipcfilu  22311  fcoinver  29741  trclubgNEW  38423  trrelsuperrel2dg  38461
  Copyright terms: Public domain W3C validator