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

Theorem coss2 5200
 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 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
21ssbrd 4626 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑦𝑥𝐵𝑦))
32anim1d 586 . . . 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:  coeq2  5202  funss  5822  tposss  7240  dftpos4  7258  rtrclreclem4  13649  tsrdir  17061  mvdco  17688  ustex2sym  21830  ustex3sym  21831  ustund  21835  ustneism  21837  trust  21843  utop2nei  21864  neipcfilu  21910  fcoinver  28798  trclubgNEW  36944  trrelsuperrel2dg  36982
 Copyright terms: Public domain W3C validator