Theorem coss2 5691

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 5074	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦))
2	1	anim1d 613	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
3	2	eximdv 1918	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
4	3	ssopab2dv 5403	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)})
5		df-co 5528	. 2 ⊢ (𝐶 ∘ 𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)}
6		df-co 5528	. 2 ⊢ (𝐶 ∘ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)}
7	4, 5, 6	3sstr4g 3960	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ⊆ wss 3881   class class class wbr 5030  {copab 5092   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-co 5528

This theorem is referenced by:  coeq2  5693  funss  6343  tposss  7876  dftpos4  7894  rtrclreclem4  14412  tsrdir  17840  mvdco  18565  ustex2sym  22822  ustex3sym  22823  ustneism  22829  trust  22835  utop2nei  22856  neipcfilu  22902  fcoinver  30370  trclubgNEW  40318  trrelsuperrel2dg  40372