Theorem iunexg 7956

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  ∀wral 3079  ∃wrex 3089  Vcvv 3455  ∪ cuni 4872  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-uni 4873  df-iun 4958

This theorem is referenced by:  abrexex2g  7957  opabex3d  7958  opabex3rd  7959  opabex3  7960  iunex  7961  xpexgALT  7974  mpoexxg  8068  ixpexg  8916  ixpssmapg  8922  ttrclselem2  9691  iundom  10521  iunctb  10554  wrdexg  14557  cshwsex  17155  imasplusg  17566  imasmulr  17567  imasvsca  17569  imasip  17570  gsum2d2  20039  gsumcom2  20040  dprd2da  20109  ptcls  23773  ptcmplem2  24210  elpwiuncl  32873  aciunf1lem  33007  gsumpart  33383  gsumwrd2dccat  33398  irngval  34075  esum2dlem  34482  esum2d  34483  esumiun  34484  omssubadd  34690  eulerpartlemgs2  34770  bnj535  35278  bnj546  35284  bnj893  35316  bnj1136  35385  bnj1413  35423  tz9.1regs  35547  weiunse  36999  numiunnum  37001  eliunov2  44425  fvmptiunrelexplb0d  44430  fvmptiunrelexplb1d  44432  iunrelexp0  44448  collexd  44987  unirnmapsn  45950  iunmapss  45951  ssmapsn  45952  iunmapsn  45953  sge0iunmptlemfi  47147  sge0iunmpt  47152  smflimlem1  47505  smfliminflem  47564  mpoexxg2  49138  imasubclem1  49902