Theorem coss1 5804

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 5130	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑧 → 𝑦𝐵𝑧))
2	1	anim2d 613	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)))
3	2	eximdv 1919	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧) → ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)))
4	3	ssopab2dv 5499	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)} ⊆ {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)})
5		df-co 5633	. 2 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐴𝑧)}
6		df-co 5633	. 2 ⊢ (𝐵 ∘ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝑥𝐶𝑦 ∧ 𝑦𝐵𝑧)}
7	4, 5, 6	3sstr4g 3976	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ⊆ wss 3890   class class class wbr 5086  {copab 5148   ∘ ccom 5628

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5633

This theorem is referenced by:  coeq1  5806  funss  6511  tposss  8170  cottrcl  9631  frmin  9664  frrlem16  9673  rtrclreclem4  15014  tsrdir  18561  ustex2sym  24192  ustex3sym  24193  ustneism  24199  trust  24204  utop2nei  24225  neipcfilu  24270  trclubgNEW  44063  trrelsuperrel2dg  44116  trclrelexplem  44156  cotrcltrcl  44170  cotrclrcl  44187  frege96d  44194  frege97d  44197  frege109d  44202  frege131d  44209