Theorem iunexg 7988

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070  Vcvv 3480  ∪ cuni 4907  ∪ ciun 4991

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 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-uni 4908  df-iun 4993

This theorem is referenced by:  abrexex2g  7989  opabex3d  7990  opabex3rd  7991  opabex3  7992  iunex  7993  xpexgALT  8006  mpoexxg  8100  ixpexg  8962  ixpssmapg  8968  ttrclselem2  9766  iundom  10582  iunctb  10614  wrdexg  14562  cshwsex  17138  imasplusg  17562  imasmulr  17563  imasvsca  17565  imasip  17566  gsum2d2  19992  gsumcom2  19993  dprd2da  20062  ptcls  23624  ptcmplem2  24061  elpwiuncl  32546  aciunf1lem  32672  gsumpart  33060  gsumwrd2dccat  33070  irngval  33735  esum2dlem  34093  esum2d  34094  esumiun  34095  omssubadd  34302  eulerpartlemgs2  34382  bnj535  34904  bnj546  34910  bnj893  34942  bnj1136  35011  bnj1413  35049  weiunse  36469  numiunnum  36471  eliunov2  43692  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  iunrelexp0  43715  collexd  44276  unirnmapsn  45219  iunmapss  45220  ssmapsn  45221  iunmapsn  45222  sge0iunmptlemfi  46428  sge0iunmpt  46433  smflimlem1  46786  smfliminflem  46845  mpoexxg2  48254