Theorem iunexg 7905

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2712  ∀wral 3049  ∃wrex 3058  Vcvv 3438  ∪ cuni 4861  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-uni 4862  df-iun 4946

This theorem is referenced by:  abrexex2g  7906  opabex3d  7907  opabex3rd  7908  opabex3  7909  iunex  7910  xpexgALT  7923  mpoexxg  8017  ixpexg  8858  ixpssmapg  8864  ttrclselem2  9633  iundom  10450  iunctb  10483  wrdexg  14445  cshwsex  17026  imasplusg  17436  imasmulr  17437  imasvsca  17439  imasip  17440  gsum2d2  19901  gsumcom2  19902  dprd2da  19971  ptcls  23558  ptcmplem2  23995  elpwiuncl  32551  aciunf1lem  32689  gsumpart  33095  gsumwrd2dccat  33109  irngval  33791  esum2dlem  34198  esum2d  34199  esumiun  34200  omssubadd  34406  eulerpartlemgs2  34486  bnj535  34995  bnj546  35001  bnj893  35033  bnj1136  35102  bnj1413  35140  tz9.1regs  35239  weiunse  36611  numiunnum  36613  eliunov2  43862  fvmptiunrelexplb0d  43867  fvmptiunrelexplb1d  43869  iunrelexp0  43885  collexd  44440  unirnmapsn  45400  iunmapss  45401  ssmapsn  45402  iunmapsn  45403  sge0iunmptlemfi  46599  sge0iunmpt  46604  smflimlem1  46957  smfliminflem  47016  mpoexxg2  48526  imasubclem1  49291