Theorem unss12 4186

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  pwssun  5542  fun  6745  f1un  6846  finsschain  9352  trclun  15173  relexpfld  15208  mulgfval  19285  mvdco  19665  dprd2da  20264  dmdprdsplit2lem  20267  lspun  21268  mulsproplem13  28520  mulsproplem14  28521  spanuni  32152  sshhococi  32154  mthmpps  36434  pibt2  38434  mblfinlem3  38671  dochdmj1  42541  mptrcllem  44707  clcnvlem  44717  dfrcl2  44768  relexpss1d  44799  corclrcl  44801  relexp0a  44810  corcltrcl  44833  frege131d  44858