Theorem unss12 4140

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3899   ⊆ wss 3901

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  pwssun  5516  fun  6696  f1un  6794  finsschain  9259  trclun  14937  relexpfld  14972  mulgfval  18999  mvdco  19374  dprd2da  19973  dmdprdsplit2lem  19976  lspun  20938  mulsproplem13  28124  mulsproplem14  28125  spanuni  31619  sshhococi  31621  mthmpps  35776  pibt2  37622  mblfinlem3  37860  dochdmj1  41650  mptrcllem  43854  clcnvlem  43864  dfrcl2  43915  relexpss1d  43946  corclrcl  43948  relexp0a  43957  corcltrcl  43980  frege131d  44005