Theorem iunexg 7960

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  ∀wral 3085  ∃wrex 3095  Vcvv 3463  ∪ cuni 4876  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-11 2198  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-mo 2573  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-uni 4877  df-iun 4962

This theorem is referenced by:  abrexex2g  7961  opabex3d  7962  opabex3rd  7963  opabex3  7964  iunex  7965  xpexgALT  7978  mpoexxg  8072  ixpexg  8920  ixpssmapg  8926  ttrclselem2  9695  iundom  10526  iunctb  10559  wrdexg  14561  cshwsex  17160  imasplusg  17571  imasmulr  17572  imasvsca  17574  imasip  17575  gsum2d2  20044  gsumcom2  20045  dprd2da  20114  ptcls  23742  ptcmplem2  24179  elpwiuncl  32814  aciunf1lem  32948  gsumpart  33324  gsumwrd2dccat  33339  irngval  34020  esum2dlem  34427  esum2d  34428  esumiun  34429  omssubadd  34635  eulerpartlemgs2  34715  bnj535  35223  bnj546  35229  bnj893  35261  bnj1136  35330  bnj1413  35368  tz9.1regs  35480  weiunse  36902  numiunnum  36904  eliunov2  44331  fvmptiunrelexplb0d  44336  fvmptiunrelexplb1d  44338  iunrelexp0  44354  collexd  44893  unirnmapsn  45856  iunmapss  45857  ssmapsn  45858  iunmapsn  45859  sge0iunmptlemfi  47053  sge0iunmpt  47058  smflimlem1  47411  smfliminflem  47470  mpoexxg2  49037  imasubclem1  49801