Theorem iunexg 7945

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2708  ∀wral 3045  ∃wrex 3054  Vcvv 3450  ∪ cuni 4874  ∪ ciun 4958

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 2702  ax-rep 5237  ax-sep 5254  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-uni 4875  df-iun 4960

This theorem is referenced by:  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  opabex3  7949  iunex  7950  xpexgALT  7963  mpoexxg  8057  ixpexg  8898  ixpssmapg  8904  ttrclselem2  9686  iundom  10502  iunctb  10534  wrdexg  14496  cshwsex  17078  imasplusg  17487  imasmulr  17488  imasvsca  17490  imasip  17491  gsum2d2  19911  gsumcom2  19912  dprd2da  19981  ptcls  23510  ptcmplem2  23947  elpwiuncl  32463  aciunf1lem  32593  gsumpart  33004  gsumwrd2dccat  33014  irngval  33687  esum2dlem  34089  esum2d  34090  esumiun  34091  omssubadd  34298  eulerpartlemgs2  34378  bnj535  34887  bnj546  34893  bnj893  34925  bnj1136  34994  bnj1413  35032  weiunse  36463  numiunnum  36465  eliunov2  43675  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  iunrelexp0  43698  collexd  44253  unirnmapsn  45215  iunmapss  45216  ssmapsn  45217  iunmapsn  45218  sge0iunmptlemfi  46418  sge0iunmpt  46423  smflimlem1  46776  smfliminflem  46835  mpoexxg2  48330  imasubclem1  49097