Theorem iunexg 7985

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  {cab 2741  ∀wral 3080  ∃wrex 3090  Vcvv 3454  ∪ cuni 4870  ∪ ciun 4954

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 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-11 2196  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-uni 4871  df-iun 4956

This theorem is used by:  abrexex2g  7986  opabex3d  7987  opabex3rd  7988  opabex3  7989  iunex  7990  xpexgALT  8003  mpoexxg  8099  ixpexg  8964  ixpssmapg  8970  ttrclselem2  9740  iundom  10639  iunctb  10672  wrdexg  14682  cshwsex  17293  imasplusg  17704  imasmulr  17705  imasvsca  17707  imasip  17708  gsum2d2  20203  gsumcom2  20204  dprd2da  20273  ptcls  23950  ptcmplem2  24387  elpwiuncl  33180  aciunf1lem  33313  gsumpart  33680  gsumwrd2dccat  33695  irngval  34373  esum2dlem  34780  esum2d  34781  esumiun  34782  omssubadd  34988  eulerpartlemgs2  35068  bnj535  35576  bnj546  35582  bnj893  35614  bnj1136  35683  bnj1413  35721  tz9.1regs  35876  weiunse  37389  numiunnum  37391  eliunov2  44825  fvmptiunrelexplb0d  44830  fvmptiunrelexplb1d  44832  iunrelexp0  44848  collexd  45387  unirnmapsn  46372  iunmapss  46373  ssmapsn  46374  iunmapsn  46375  sge0iunmptlemfi  47568  sge0iunmpt  47573  smflimlem1  47926  smfliminflem  47985  mpoexxg2  49595  imasubclem1  50365