Theorem coss2 5844

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 5156	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦))
2	1	anim1d 622	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
3	2	eximdv 1947	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
4	3	ssopab2dv 5538	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)})
5		df-co 5672	. 2 ⊢ (𝐶 ∘ 𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)}
6		df-co 5672	. 2 ⊢ (𝐶 ∘ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)}
7	4, 5, 6	3sstr4g 3991	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809   ⊆ wss 3906   class class class wbr 5110  {copab 5174   ∘ ccom 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-br 5111  df-opab 5175  df-co 5672

This theorem is referenced by:  coeq2  5846  funss  6557  tposss  8224  dftpos4  8242  ttrclco  9688  frmin  9722  frrlem16  9731  rtrclreclem4  15100  tsrdir  18661  mvdco  19516  ustex2sym  24355  ustex3sym  24356  ustneism  24362  trust  24367  utop2nei  24388  neipcfilu  24433  fcoinver  32930  trclubgNEW  44327  trrelsuperrel2dg  44380