Theorem uniss 4566

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 3703	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 590	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1959	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4547	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4547	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 3715	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1817   ∈ wcel 2103   ⊆ wss 3680  ∪ cuni 4544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-in 3687  df-ss 3694  df-uni 4545

This theorem is referenced by:  unissi  4569  unissd  4570  intssuni2  4610  uniintsn  4622  relfld  5774  dffv2  6385  trcl  8717  cflm  9185  coflim  9196  cfslbn  9202  fin23lem41  9287  fin1a2lem12  9346  tskuni  9718  prdsval  16238  prdsbas  16240  prdsplusg  16241  prdsmulr  16242  prdsvsca  16243  prdshom  16250  mrcssv  16397  catcfuccl  16881  catcxpccl  16969  mrelatlub  17308  mreclatBAD  17309  dprdres  18548  dmdprdsplit2lem  18565  tgcl  20896  distop  20922  fctop  20931  cctop  20933  neiptoptop  21058  cmpcld  21328  uncmp  21329  cmpfi  21334  comppfsc  21458  kgentopon  21464  txcmplem2  21568  filconn  21809  alexsubALTlem3  21975  alexsubALT  21977  ptcmplem3  21980  dyadmbllem  23488  shsupcl  28427  hsupss  28430  shatomistici  29450  pwuniss  29598  carsggect  30610  carsgclctun  30613  cvmliftlem15  31508  frrlem5c  32013  filnetlem3  32602  icoreunrn  33439  heiborlem1  33842  lssats  34719  lpssat  34720  lssatle  34722  lssat  34723  dicval  36884  pwsal  40955  prsal  40958  intsaluni  40967