Theorem iunexg 7975

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2739  ∀wral 3077  ∃wrex 3087  Vcvv 3451  ∪ cuni 4867  ∪ ciun 4951

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 2147  ax-9 2155  ax-11 2194  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-uni 4868  df-iun 4953

This theorem is used by:  abrexex2g  7976  opabex3d  7977  opabex3rd  7978  opabex3  7979  iunex  7980  xpexgALT  7993  mpoexxg  8088  ixpexg  8950  ixpssmapg  8956  ttrclselem2  9727  iundom  10626  iunctb  10659  wrdexg  14669  cshwsex  17278  imasplusg  17689  imasmulr  17690  imasvsca  17692  imasip  17693  gsum2d2  20188  gsumcom2  20189  dprd2da  20258  ptcls  23935  ptcmplem2  24372  elpwiuncl  33123  aciunf1lem  33256  gsumpart  33624  gsumwrd2dccat  33639  irngval  34317  esum2dlem  34724  esum2d  34725  esumiun  34726  omssubadd  34932  eulerpartlemgs2  35012  bnj535  35520  bnj546  35526  bnj893  35558  bnj1136  35627  bnj1413  35665  tz9.1regs  35802  weiunse  37256  numiunnum  37258  eliunov2  44678  fvmptiunrelexplb0d  44683  fvmptiunrelexplb1d  44685  iunrelexp0  44701  collexd  45240  unirnmapsn  46226  iunmapss  46227  ssmapsn  46228  iunmapsn  46229  sge0iunmptlemfi  47422  sge0iunmpt  47427  smflimlem1  47780  smfliminflem  47839  mpoexxg2  49449  imasubclem1  50211