Theorem iunexg 7970

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {cab 2712  ∀wral 3050  ∃wrex 3059  Vcvv 3463  ∪ cuni 4887  ∪ ciun 4971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-11 2156  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-mo 2538  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-v 3465  df-ss 3948  df-uni 4888  df-iun 4973

This theorem is referenced by:  abrexex2g  7971  opabex3d  7972  opabex3rd  7973  opabex3  7974  iunex  7975  xpexgALT  7988  mpoexxg  8082  ixpexg  8944  ixpssmapg  8950  ttrclselem2  9748  iundom  10564  iunctb  10596  wrdexg  14545  cshwsex  17121  imasplusg  17534  imasmulr  17535  imasvsca  17537  imasip  17538  gsum2d2  19961  gsumcom2  19962  dprd2da  20031  ptcls  23571  ptcmplem2  24008  elpwiuncl  32475  aciunf1lem  32608  gsumpart  33004  gsumwrd2dccat  33014  irngval  33677  esum2dlem  34068  esum2d  34069  esumiun  34070  omssubadd  34277  eulerpartlemgs2  34357  bnj535  34879  bnj546  34885  bnj893  34917  bnj1136  34986  bnj1413  35024  weiunse  36444  numiunnum  36446  eliunov2  43669  fvmptiunrelexplb0d  43674  fvmptiunrelexplb1d  43676  iunrelexp0  43692  collexd  44248  unirnmapsn  45191  iunmapss  45192  ssmapsn  45193  iunmapsn  45194  sge0iunmptlemfi  46400  sge0iunmpt  46405  smflimlem1  46758  smfliminflem  46817  mpoexxg2  48227