Theorem coss2 5881

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 5210	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑥𝐴𝑦 → 𝑥𝐵𝑦))
2	1	anim1d 610	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
3	2	eximdv 1916	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧) → ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)))
4	3	ssopab2dv 5570	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)})
5		df-co 5709	. 2 ⊢ (𝐶 ∘ 𝐴) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐴𝑦 ∧ 𝑦𝐶𝑧)}
6		df-co 5709	. 2 ⊢ (𝐶 ∘ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐵𝑦 ∧ 𝑦𝐶𝑧)}
7	4, 5, 6	3sstr4g 4054	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ⊆ wss 3976   class class class wbr 5166  {copab 5228   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq2  5883  funss  6597  tposss  8268  dftpos4  8286  ttrclco  9787  frmin  9818  frrlem16  9827  rtrclreclem4  15110  tsrdir  18674  mvdco  19487  ustex2sym  24246  ustex3sym  24247  ustneism  24253  trust  24259  utop2nei  24280  neipcfilu  24326  fcoinver  32626  trclubgNEW  43580  trrelsuperrel2dg  43633