Theorem iunexg 7942

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  Vcvv 3447  ∪ cuni 4871  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-uni 4872  df-iun 4957

This theorem is referenced by:  abrexex2g  7943  opabex3d  7944  opabex3rd  7945  opabex3  7946  iunex  7947  xpexgALT  7960  mpoexxg  8054  ixpexg  8895  ixpssmapg  8901  ttrclselem2  9679  iundom  10495  iunctb  10527  wrdexg  14489  cshwsex  17071  imasplusg  17480  imasmulr  17481  imasvsca  17483  imasip  17484  gsum2d2  19904  gsumcom2  19905  dprd2da  19974  ptcls  23503  ptcmplem2  23940  elpwiuncl  32456  aciunf1lem  32586  gsumpart  32997  gsumwrd2dccat  33007  irngval  33680  esum2dlem  34082  esum2d  34083  esumiun  34084  omssubadd  34291  eulerpartlemgs2  34371  bnj535  34880  bnj546  34886  bnj893  34918  bnj1136  34987  bnj1413  35025  weiunse  36456  numiunnum  36458  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  iunrelexp0  43691  collexd  44246  unirnmapsn  45208  iunmapss  45209  ssmapsn  45210  iunmapsn  45211  sge0iunmptlemfi  46411  sge0iunmpt  46416  smflimlem1  46769  smfliminflem  46828  mpoexxg2  48326  imasubclem1  49093