Theorem iunexg 7945

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  {cab 2741  ∀wral 3077  ∃wrex 3087  Vcvv 3455  ∪ cuni 4866  ∪ ciun 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-v 3457  df-ss 3922  df-uni 4867  df-iun 4952

This theorem is referenced by:  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  opabex3  7949  iunex  7950  xpexgALT  7963  mpoexxg  8057  ixpexg  8905  ixpssmapg  8911  ttrclselem2  9682  iundom  10500  iunctb  10533  wrdexg  14538  cshwsex  17137  imasplusg  17548  imasmulr  17549  imasvsca  17551  imasip  17552  gsum2d2  20015  gsumcom2  20016  dprd2da  20085  ptcls  23677  ptcmplem2  24114  elpwiuncl  32727  aciunf1lem  32865  gsumpart  33244  gsumwrd2dccat  33259  irngval  33983  esum2dlem  34390  esum2d  34391  esumiun  34392  omssubadd  34598  eulerpartlemgs2  34678  bnj535  35186  bnj546  35192  bnj893  35224  bnj1136  35293  bnj1413  35331  tz9.1regs  35431  weiunse  36829  numiunnum  36831  eliunov2  44256  fvmptiunrelexplb0d  44261  fvmptiunrelexplb1d  44263  iunrelexp0  44279  collexd  44834  unirnmapsn  45791  iunmapss  45792  ssmapsn  45793  iunmapsn  45794  sge0iunmptlemfi  46988  sge0iunmpt  46993  smflimlem1  47346  smfliminflem  47405  mpoexxg2  48961  imasubclem1  49726