Theorem coss1 5880

Description: Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)

Assertion

Ref	Expression
coss1	⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))

Proof of Theorem coss1

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssbr 5210	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑧 → 𝑦𝐵𝑧))
2	1	anim2d 611	. . . 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:  coeq1  5882  funss  6597  tposss  8268  cottrcl  9788  frmin  9818  frrlem16  9827  rtrclreclem4  15110  tsrdir  18674  ustex2sym  24246  ustex3sym  24247  ustneism  24253  trust  24259  utop2nei  24280  neipcfilu  24326  trclubgNEW  43580  trrelsuperrel2dg  43633  trclrelexplem  43673  cotrcltrcl  43687  cotrclrcl  43704  frege96d  43711  frege97d  43714  frege109d  43719  frege131d  43726