Theorem unss1 4165

Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
unss1	⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))

Proof of Theorem unss1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3957	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	orim1d 967	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4133	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4133	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) → 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	ssrdv 3969	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 847   ∈ wcel 2109   ∪ cun 3929   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  unss2  4167  unss12  4168  eldifpw  7767  orderseqlem  8161  tposss  8231  dftpos4  8249  hashbclem  14475  incexclem  15857  mreexexlem2d  17662  catcoppccl  18135  neitr  23123  restntr  23125  leordtval2  23155  cmpcld  23345  uniioombllem3  25543  limcres  25844  plyss  26161  mulsproplem13  28088  mulsproplem14  28089  shlej1  31346  fineqvac  35133  ss2mcls  35595  bj-rrhatsscchat  37259  pclfinclN  39974  dmtposss  48818