Theorem unss1 4182

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 3903	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	orim1d 981	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4151	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4151	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) → 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	ssrdv 3915	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   ∈ wcel 2144   ⊆ wss 3896   ∪ cun 4148

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 3897  df-un 4150

This theorem is used by:  unss2  4184  unss12  4185  eldifpw  7786  orderseqlem  8180  tposss  8251  dftpos4  8269  hashbclem  14604  incexclem  16014  mreexexlem2d  17828  catcoppccl  18301  neitr  23507  restntr  23509  leordtval2  23539  cmpcld  23729  uniioombllem3  25915  limcres  26215  plyss  26526  mulsproplem13  28523  mulsproplem14  28524  shlej1  31971  fineqvac  35844  ss2mcls  36423  bj-rrhatsscchat  38266  pclfinclN  41116  dmtposss  50097