Theorem iunexg 7966

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 4996	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2	1	adantl 487	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
3		abrexexg 7964	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
4	3	uniexd 7750	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
5	4	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
6	2, 5	eqeltrd 2865	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {cab 2743  ∀wral 3081  ∃wrex 3091  Vcvv 3457  ∪ cuni 4874  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-11 2195  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-uni 4875  df-iun 4960

This theorem is used by:  abrexex2g  7967  opabex3d  7968  opabex3rd  7969  opabex3  7970  iunex  7971  xpexgALT  7984  mpoexxg  8078  ixpexg  8926  ixpssmapg  8932  ttrclselem2  9702  iundom  10545  iunctb  10578  wrdexg  14583  cshwsex  17186  imasplusg  17597  imasmulr  17598  imasvsca  17600  imasip  17601  gsum2d2  20092  gsumcom2  20093  dprd2da  20162  ptcls  23828  ptcmplem2  24265  elpwiuncl  32948  aciunf1lem  33082  gsumpart  33451  gsumwrd2dccat  33466  irngval  34143  esum2dlem  34550  esum2d  34551  esumiun  34552  omssubadd  34759  eulerpartlemgs2  34839  bnj535  35347  bnj546  35353  bnj893  35385  bnj1136  35454  bnj1413  35492  tz9.1regs  35608  weiunse  37040  numiunnum  37042  eliunov2  44482  fvmptiunrelexplb0d  44487  fvmptiunrelexplb1d  44489  iunrelexp0  44505  collexd  45044  unirnmapsn  46007  iunmapss  46008  ssmapsn  46009  iunmapsn  46010  sge0iunmptlemfi  47204  sge0iunmpt  47209  smflimlem1  47562  smfliminflem  47621  mpoexxg2  49194  imasubclem1  49958