Theorem iunexg 7898

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  Vcvv 3436  ∪ cuni 4858  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3438  df-ss 3920  df-uni 4859  df-iun 4943

This theorem is referenced by:  abrexex2g  7899  opabex3d  7900  opabex3rd  7901  opabex3  7902  iunex  7903  xpexgALT  7916  mpoexxg  8010  ixpexg  8849  ixpssmapg  8855  ttrclselem2  9622  iundom  10436  iunctb  10468  wrdexg  14431  cshwsex  17012  imasplusg  17421  imasmulr  17422  imasvsca  17424  imasip  17425  gsum2d2  19853  gsumcom2  19854  dprd2da  19923  ptcls  23501  ptcmplem2  23938  elpwiuncl  32471  aciunf1lem  32606  gsumpart  33011  gsumwrd2dccat  33021  irngval  33658  esum2dlem  34065  esum2d  34066  esumiun  34067  omssubadd  34274  eulerpartlemgs2  34354  bnj535  34863  bnj546  34869  bnj893  34901  bnj1136  34970  bnj1413  35008  tz9.1regs  35073  weiunse  36452  numiunnum  36454  eliunov2  43662  fvmptiunrelexplb0d  43667  fvmptiunrelexplb1d  43669  iunrelexp0  43685  collexd  44240  unirnmapsn  45202  iunmapss  45203  ssmapsn  45204  iunmapsn  45205  sge0iunmptlemfi  46404  sge0iunmpt  46409  smflimlem1  46762  smfliminflem  46821  mpoexxg2  48332  imasubclem1  49099