Theorem iunexg 7906

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 4960	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2	1	adantl 482	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
3		abrexexg 7904	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
4	3	uniexd 7686	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
5	4	adantr 481	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
6	2, 5	eqeltrd 2839	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2717  ∀wral 3053  ∃wrex 3063  Vcvv 3431  ∪ cuni 4839  ∪ ciun 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-ext 2711  ax-rep 5200  ax-sep 5219  ax-un 7679

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-uni 4840  df-iun 4924

This theorem is referenced by:  abrexex2g  7907  opabex3d  7908  opabex3rd  7909  opabex3  7910  iunex  7911  xpexgALT  7924  mpoexxg  8018  ixpexg  8861  ixpssmapg  8867  ttrclselem2  9639  iundom  10456  iunctb  10489  wrdexg  14478  cshwsex  17063  imasplusg  17473  imasmulr  17474  imasvsca  17476  imasip  17477  gsum2d2  19941  gsumcom2  19942  dprd2da  20011  ptcls  23600  ptcmplem2  24037  elpwiuncl  32616  aciunf1lem  32755  gsumpart  33145  gsumwrd2dccat  33160  irngval  33878  esum2dlem  34285  esum2d  34286  esumiun  34287  omssubadd  34493  eulerpartlemgs2  34573  bnj535  35081  bnj546  35087  bnj893  35119  bnj1136  35188  bnj1413  35226  tz9.1regs  35324  weiunse  36705  numiunnum  36707  eliunov2  44132  fvmptiunrelexplb0d  44137  fvmptiunrelexplb1d  44139  iunrelexp0  44155  collexd  44710  unirnmapsn  45667  iunmapss  45668  ssmapsn  45669  iunmapsn  45670  sge0iunmptlemfi  46864  sge0iunmpt  46869  smflimlem1  47222  smfliminflem  47281  mpoexxg2  48837  imasubclem1  49602