Theorem iunexg 7961

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450  ∪ cuni 4867  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-uni 4868  df-iun 4953

This theorem is used by:  abrexex2g  7962  opabex3d  7963  opabex3rd  7964  opabex3  7965  iunex  7966  xpexgALT  7979  mpoexxg  8075  ixpexg  8932  ixpssmapg  8938  ttrclselem2  9708  iundom  10553  iunctb  10586  wrdexg  14592  cshwsex  17195  imasplusg  17606  imasmulr  17607  imasvsca  17609  imasip  17610  gsum2d2  20104  gsumcom2  20105  dprd2da  20174  ptcls  23845  ptcmplem2  24282  elpwiuncl  33005  aciunf1lem  33138  gsumpart  33506  gsumwrd2dccat  33521  irngval  34198  esum2dlem  34605  esum2d  34606  esumiun  34607  omssubadd  34814  eulerpartlemgs2  34894  bnj535  35402  bnj546  35408  bnj893  35440  bnj1136  35509  bnj1413  35547  tz9.1regs  35663  weiunse  37090  numiunnum  37092  eliunov2  44522  fvmptiunrelexplb0d  44527  fvmptiunrelexplb1d  44529  iunrelexp0  44545  collexd  45084  unirnmapsn  46047  iunmapss  46048  ssmapsn  46049  iunmapsn  46050  sge0iunmptlemfi  47244  sge0iunmpt  47249  smflimlem1  47602  smfliminflem  47661  mpoexxg2  49271  imasubclem1  50033