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 4987	. . 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 2860	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450  ∪ cuni 4866  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3914  df-uni 4867  df-iun 4952

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  44679  fvmptiunrelexplb0d  44684  fvmptiunrelexplb1d  44686  iunrelexp0  44702  collexd  45241  unirnmapsn  46227  iunmapss  46228  ssmapsn  46229  iunmapsn  46230  sge0iunmptlemfi  47423  sge0iunmpt  47428  smflimlem1  47781  smfliminflem  47840  mpoexxg2  49450  imasubclem1  50212