Theorem iunexg 7962

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2713  ∀wral 3051  ∃wrex 3060  Vcvv 3459  ∪ cuni 4883  ∪ ciun 4967

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 2707  ax-rep 5249  ax-sep 5266  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-uni 4884  df-iun 4969

This theorem is referenced by:  abrexex2g  7963  opabex3d  7964  opabex3rd  7965  opabex3  7966  iunex  7967  xpexgALT  7980  mpoexxg  8074  ixpexg  8936  ixpssmapg  8942  ttrclselem2  9740  iundom  10556  iunctb  10588  wrdexg  14542  cshwsex  17120  imasplusg  17531  imasmulr  17532  imasvsca  17534  imasip  17535  gsum2d2  19955  gsumcom2  19956  dprd2da  20025  ptcls  23554  ptcmplem2  23991  elpwiuncl  32508  aciunf1lem  32640  gsumpart  33051  gsumwrd2dccat  33061  irngval  33726  esum2dlem  34123  esum2d  34124  esumiun  34125  omssubadd  34332  eulerpartlemgs2  34412  bnj535  34921  bnj546  34927  bnj893  34959  bnj1136  35028  bnj1413  35066  weiunse  36486  numiunnum  36488  eliunov2  43703  fvmptiunrelexplb0d  43708  fvmptiunrelexplb1d  43710  iunrelexp0  43726  collexd  44281  unirnmapsn  45238  iunmapss  45239  ssmapsn  45240  iunmapsn  45241  sge0iunmptlemfi  46442  sge0iunmpt  46447  smflimlem1  46800  smfliminflem  46859  mpoexxg2  48313  imasubclem1  49063