Theorem iunexg 7907

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  ∀wral 3051  ∃wrex 3060  Vcvv 3440  ∪ cuni 4863  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-uni 4864  df-iun 4948

This theorem is referenced by:  abrexex2g  7908  opabex3d  7909  opabex3rd  7910  opabex3  7911  iunex  7912  xpexgALT  7925  mpoexxg  8019  ixpexg  8862  ixpssmapg  8868  ttrclselem2  9637  iundom  10454  iunctb  10487  wrdexg  14449  cshwsex  17030  imasplusg  17440  imasmulr  17441  imasvsca  17443  imasip  17444  gsum2d2  19905  gsumcom2  19906  dprd2da  19975  ptcls  23562  ptcmplem2  23999  elpwiuncl  32604  aciunf1lem  32742  gsumpart  33148  gsumwrd2dccat  33162  irngval  33844  esum2dlem  34251  esum2d  34252  esumiun  34253  omssubadd  34459  eulerpartlemgs2  34539  bnj535  35048  bnj546  35054  bnj893  35086  bnj1136  35155  bnj1413  35193  tz9.1regs  35292  weiunse  36664  numiunnum  36666  eliunov2  43941  fvmptiunrelexplb0d  43946  fvmptiunrelexplb1d  43948  iunrelexp0  43964  collexd  44519  unirnmapsn  45479  iunmapss  45480  ssmapsn  45481  iunmapsn  45482  sge0iunmptlemfi  46678  sge0iunmpt  46683  smflimlem1  47036  smfliminflem  47095  mpoexxg2  48605  imasubclem1  49370