Theorem unss12 4211

Description: Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)

Assertion

Ref	Expression
unss12	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))

Proof of Theorem unss12

Step	Hyp	Ref	Expression
1		unss1 4208	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
2		unss2 4210	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
3	1, 2	sylan9ss 4022	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3974   ⊆ wss 3976

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-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  pwssun  5590  fun  6783  f1un  6882  undomOLD  9126  finsschain  9429  trclun  15063  relexpfld  15098  mulgfval  19109  mvdco  19487  dprd2da  20086  dmdprdsplit2lem  20089  lspun  21008  mulsproplem13  28172  mulsproplem14  28173  spanuni  31576  sshhococi  31578  mthmpps  35550  pibt2  37383  mblfinlem3  37619  dochdmj1  41347  mptrcllem  43575  clcnvlem  43585  dfrcl2  43636  relexpss1d  43667  corclrcl  43669  relexp0a  43678  corcltrcl  43701  frege131d  43726