Theorem unss12 4141

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∪ cun 3904   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  pwssun  5555  fun  6744  f1un  6845  finsschain  9319  trclun  15070  relexpfld  15105  mulgfval  19158  mvdco  19538  dprd2da  20137  dmdprdsplit2lem  20140  lspun  21137  mulsproplem13  28350  mulsproplem14  28351  spanuni  31925  sshhococi  31927  mthmpps  36087  pibt2  38096  mblfinlem3  38343  dochdmj1  42197  mptrcllem  44372  clcnvlem  44382  dfrcl2  44433  relexpss1d  44464  corclrcl  44466  relexp0a  44475  corcltrcl  44498  frege131d  44523