Theorem iunexg 7947

Description: The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.)

Assertion

Ref	Expression
iunexg	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem iunexg

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfiun2g 5033	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2	1	adantl 483	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
3		abrexexg 7944	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
4	3	uniexd 7729	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
5	4	adantr 482	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
6	2, 5	eqeltrd 2834	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  ∀wral 3062  ∃wrex 3071  Vcvv 3475  ∪ cuni 4908  ∪ ciun 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-mo 2535  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-in 3955  df-ss 3965  df-uni 4909  df-iun 4999

This theorem is referenced by:  abrexex2g  7948  opabex3d  7949  opabex3rd  7950  opabex3  7951  iunex  7952  xpexgALT  7965  mpoexxg  8059  ixpexg  8913  ixpssmapg  8919  ttrclselem2  9718  iundom  10534  iunctb  10566  wrdexg  14471  cshwsex  17031  imasplusg  17460  imasmulr  17461  imasvsca  17463  imasip  17464  gsum2d2  19837  gsumcom2  19838  dprd2da  19907  ptcls  23112  ptcmplem2  23549  elpwiuncl  31753  aciunf1lem  31875  gsumpart  32195  irngval  32738  esum2dlem  33079  esum2d  33080  esumiun  33081  omssubadd  33288  eulerpartlemgs2  33368  bnj535  33890  bnj546  33896  bnj893  33928  bnj1136  33997  bnj1413  34035  eliunov2  42416  fvmptiunrelexplb0d  42421  fvmptiunrelexplb1d  42423  iunrelexp0  42439  collexd  43002  unirnmapsn  43899  iunmapss  43900  ssmapsn  43901  iunmapsn  43902  sge0iunmptlemfi  45116  sge0iunmpt  45121  smflimlem1  45474  smfliminflem  45533  mpoexxg2  46967