Theorem iunexg 7895

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∃wrex 3056  Vcvv 3436  ∪ cuni 4856  ∪ ciun 4939

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 2113  ax-9 2121  ax-11 2160  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-ss 3914  df-uni 4857  df-iun 4941

This theorem is referenced by:  abrexex2g  7896  opabex3d  7897  opabex3rd  7898  opabex3  7899  iunex  7900  xpexgALT  7913  mpoexxg  8007  ixpexg  8846  ixpssmapg  8852  ttrclselem2  9616  iundom  10433  iunctb  10465  wrdexg  14431  cshwsex  17012  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  gsum2d2  19886  gsumcom2  19887  dprd2da  19956  ptcls  23531  ptcmplem2  23968  elpwiuncl  32507  aciunf1lem  32644  gsumpart  33037  gsumwrd2dccat  33047  irngval  33698  esum2dlem  34105  esum2d  34106  esumiun  34107  omssubadd  34313  eulerpartlemgs2  34393  bnj535  34902  bnj546  34908  bnj893  34940  bnj1136  35009  bnj1413  35047  tz9.1regs  35130  weiunse  36512  numiunnum  36514  eliunov2  43782  fvmptiunrelexplb0d  43787  fvmptiunrelexplb1d  43789  iunrelexp0  43805  collexd  44360  unirnmapsn  45321  iunmapss  45322  ssmapsn  45323  iunmapsn  45324  sge0iunmptlemfi  46521  sge0iunmpt  46526  smflimlem1  46879  smfliminflem  46938  mpoexxg2  48448  imasubclem1  49215