Theorem unss1 4148

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 3940	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	orim1d 967	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4116	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4116	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) → 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	ssrdv 3952	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  unss2  4150  unss12  4151  eldifpw  7744  orderseqlem  8136  tposss  8206  dftpos4  8224  hashbclem  14417  incexclem  15802  mreexexlem2d  17606  catcoppccl  18079  neitr  23067  restntr  23069  leordtval2  23099  cmpcld  23289  uniioombllem3  25486  limcres  25787  plyss  26104  mulsproplem13  28031  mulsproplem14  28032  shlej1  31289  fineqvac  35087  ss2mcls  35555  bj-rrhatsscchat  37224  pclfinclN  39944  dmtposss  48864