Theorem uniss 4388

Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
uniss	⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Proof of Theorem uniss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3561	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 586	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1832	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4369	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4369	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 283	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3573	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 382  ∃wex 1694   ∈ wcel 1976   ⊆ wss 3539  ∪ cuni 4366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-uni 4367

This theorem is referenced by:  unissi  4391  unissd  4392  intssuni2  4431  uniintsn  4443  relfld  5564  dffv2  6166  trcl  8464  cflm  8932  coflim  8943  cfslbn  8949  fin23lem41  9034  fin1a2lem12  9093  tskuni  9461  prdsval  15884  prdsbas  15886  prdsplusg  15887  prdsmulr  15888  prdsvsca  15889  prdshom  15896  mrcssv  16043  catcfuccl  16528  catcxpccl  16616  mrelatlub  16955  mreclatBAD  16956  dprdres  18196  dmdprdsplit2lem  18213  tgcl  20526  distop  20552  fctop  20560  cctop  20562  neiptoptop  20687  cmpcld  20957  uncmp  20958  cmpfi  20963  comppfsc  21087  kgentopon  21093  txcmplem2  21197  filcon  21439  alexsubALTlem3  21605  alexsubALT  21607  ptcmplem3  21610  dyadmbllem  23090  shsupcl  27387  hsupss  27390  shatomistici  28410  pwuniss  28559  carsggect  29513  carsgclctun  29516  cvmliftlem15  30340  frrlem5c  30836  filnetlem3  31351  icoreunrn  32179  heiborlem1  32576  lssats  33113  lpssat  33114  lssatle  33116  lssat  33117  dicval  35279  pwsal  39008  prsal  39011  intsaluni  39020