Theorem iunexg 7918

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  Vcvv 3430  ∪ cuni 4851  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-uni 4852  df-iun 4936

This theorem is referenced by:  abrexex2g  7919  opabex3d  7920  opabex3rd  7921  opabex3  7922  iunex  7923  xpexgALT  7936  mpoexxg  8030  ixpexg  8872  ixpssmapg  8878  ttrclselem2  9649  iundom  10466  iunctb  10499  wrdexg  14488  cshwsex  17073  imasplusg  17483  imasmulr  17484  imasvsca  17486  imasip  17487  gsum2d2  19951  gsumcom2  19952  dprd2da  20021  ptcls  23583  ptcmplem2  24020  elpwiuncl  32599  aciunf1lem  32737  gsumpart  33126  gsumwrd2dccat  33141  irngval  33831  esum2dlem  34238  esum2d  34239  esumiun  34240  omssubadd  34446  eulerpartlemgs2  34526  bnj535  35034  bnj546  35040  bnj893  35072  bnj1136  35141  bnj1413  35179  tz9.1regs  35280  weiunse  36652  numiunnum  36654  eliunov2  44108  fvmptiunrelexplb0d  44113  fvmptiunrelexplb1d  44115  iunrelexp0  44131  collexd  44686  unirnmapsn  45645  iunmapss  45646  ssmapsn  45647  iunmapsn  45648  sge0iunmptlemfi  46843  sge0iunmpt  46848  smflimlem1  47201  smfliminflem  47260  mpoexxg2  48816  imasubclem1  49581