Theorem coss2 5802

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.

Step	Hyp	Ref	Expression
1		ssbr 5139	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦))
2	1	anim1d 611	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
3	2	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
4	3	ssopab2dv 5496	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)})
5		df-co 5630	. 2 ⊢ (𝐶 ∘ 𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)}
6		df-co 5630	. 2 ⊢ (𝐶 ∘ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)}
7	4, 5, 6	3sstr4g 3984	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ⊆ wss 3898   class class class wbr 5095  {copab 5157   ∘ ccom 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-br 5096  df-opab 5158  df-co 5630

This theorem is referenced by:  coeq2  5804  funss  6508  tposss  8166  dftpos4  8184  ttrclco  9619  frmin  9653  frrlem16  9662  rtrclreclem4  14975  tsrdir  18518  mvdco  19365  ustex2sym  24152  ustex3sym  24153  ustneism  24159  trust  24164  utop2nei  24185  neipcfilu  24230  fcoinver  32605  trclubgNEW  43775  trrelsuperrel2dg  43828