Theorem unss12 4187

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 4184	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))
2		unss2 4186	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))
3	1, 2	sylan9ss 3996	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3948   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967

This theorem is referenced by:  pwssun  5574  fun  6769  f1un  6867  undomOLD  9101  finsschain  9400  trclun  15054  relexpfld  15089  mulgfval  19088  mvdco  19464  dprd2da  20063  dmdprdsplit2lem  20066  lspun  20986  mulsproplem13  28155  mulsproplem14  28156  spanuni  31564  sshhococi  31566  mthmpps  35588  pibt2  37419  mblfinlem3  37667  dochdmj1  41393  mptrcllem  43631  clcnvlem  43641  dfrcl2  43692  relexpss1d  43723  corclrcl  43725  relexp0a  43734  corcltrcl  43757  frege131d  43782