Theorem coss1 5726

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ⊆ wss 3936   class class class wbr 5066  {copab 5128   ∘ ccom 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-co 5564

This theorem is referenced by:  coeq1  5728  funss  6374  tposss  7893  rtrclreclem4  14420  tsrdir  17848  ustex2sym  22825  ustex3sym  22826  ustneism  22832  trust  22838  utop2nei  22859  neipcfilu  22905  trclubgNEW  39998  trrelsuperrel2dg  40036  trclrelexplem  40076  cotrcltrcl  40090  cotrclrcl  40107  frege96d  40114  frege97d  40117  frege109d  40122  frege131d  40129