Theorem uniss 4919

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 3988	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
2	1	anim2d 612	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
3	2	eximdv 1914	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
4		eluni 4914	. . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
5		eluni 4914	. . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵))
7	6	ssrdv 4000	1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1775   ∈ wcel 2105   ⊆ wss 3962  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  unissi  4920  unissd  4921  intssuni2  4977  uniintsn  4989  relfld  6296  dffv2  7003  trcl  9765  cflm  10287  coflim  10298  cfslbn  10304  fin23lem41  10389  fin1a2lem12  10448  tskuni  10820  prdsvallem  17500  prdsval  17501  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  mrcssv  17658  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  mrelatlub  18619  mreclatBAD  18620  dprdres  20062  dmdprdsplit2lem  20079  tgcl  22991  distop  23017  fctop  23026  cctop  23028  neiptoptop  23154  cmpcld  23425  uncmp  23426  cmpfi  23431  comppfsc  23555  kgentopon  23561  txcmplem2  23665  filconn  23906  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem3  24077  dyadmbllem  25647  shsupcl  31366  hsupss  31369  shatomistici  32389  carsggect  34299  cvmliftlem15  35282  filnetlem3  36362  icoreunrn  37341  ctbssinf  37388  pibt2  37399  heiborlem1  37797  lssats  38993  lpssat  38994  lssatle  38996  lssat  38997  dicval  41158  onsupneqmaxlim0  43212  onsupnmax  43216  onsssupeqcond  43269  mreuniss  48695