Theorem iunexg 7910

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 7908	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
4	3	uniexd 7690	. . 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 7683

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  7911  opabex3d  7912  opabex3rd  7913  opabex3  7914  iunex  7915  xpexgALT  7928  mpoexxg  8022  ixpexg  8864  ixpssmapg  8870  ttrclselem2  9641  iundom  10458  iunctb  10491  wrdexg  14480  cshwsex  17065  imasplusg  17475  imasmulr  17476  imasvsca  17478  imasip  17479  gsum2d2  19943  gsumcom2  19944  dprd2da  20013  ptcls  23594  ptcmplem2  24031  elpwiuncl  32615  aciunf1lem  32753  gsumpart  33142  gsumwrd2dccat  33157  irngval  33848  esum2dlem  34255  esum2d  34256  esumiun  34257  omssubadd  34463  eulerpartlemgs2  34543  bnj535  35051  bnj546  35057  bnj893  35089  bnj1136  35158  bnj1413  35196  tz9.1regs  35297  weiunse  36669  numiunnum  36671  eliunov2  44127  fvmptiunrelexplb0d  44132  fvmptiunrelexplb1d  44134  iunrelexp0  44150  collexd  44705  unirnmapsn  45664  iunmapss  45665  ssmapsn  45666  iunmapsn  45667  sge0iunmptlemfi  46862  sge0iunmpt  46867  smflimlem1  47220  smfliminflem  47279  mpoexxg2  48829  imasubclem1  49594