Theorem iunexg 7917

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  Vcvv 3442  ∪ cuni 4865  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-uni 4866  df-iun 4950

This theorem is referenced by:  abrexex2g  7918  opabex3d  7919  opabex3rd  7920  opabex3  7921  iunex  7922  xpexgALT  7935  mpoexxg  8029  ixpexg  8872  ixpssmapg  8878  ttrclselem2  9647  iundom  10464  iunctb  10497  wrdexg  14459  cshwsex  17040  imasplusg  17450  imasmulr  17451  imasvsca  17453  imasip  17454  gsum2d2  19918  gsumcom2  19919  dprd2da  19988  ptcls  23575  ptcmplem2  24012  elpwiuncl  32618  aciunf1lem  32756  gsumpart  33161  gsumwrd2dccat  33176  irngval  33867  esum2dlem  34274  esum2d  34275  esumiun  34276  omssubadd  34482  eulerpartlemgs2  34562  bnj535  35070  bnj546  35076  bnj893  35108  bnj1136  35177  bnj1413  35215  tz9.1regs  35316  weiunse  36688  numiunnum  36690  eliunov2  44039  fvmptiunrelexplb0d  44044  fvmptiunrelexplb1d  44046  iunrelexp0  44062  collexd  44617  unirnmapsn  45576  iunmapss  45577  ssmapsn  45578  iunmapsn  45579  sge0iunmptlemfi  46775  sge0iunmpt  46780  smflimlem1  47133  smfliminflem  47192  mpoexxg2  48702  imasubclem1  49467