Theorem iunex 7950

Description: The existence of an indexed union. 𝑥 is normally a free-variable parameter in the class expression substituted for 𝐵, which can be read informally as 𝐵(𝑥). (Contributed by NM, 13-Oct-2003.)

Hypotheses

Ref	Expression
iunex.1	⊢ 𝐴 ∈ V
iunex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
iunex	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunex

Step	Hyp	Ref	Expression
1		iunex.1	. 2 ⊢ 𝐴 ∈ V
2		iunex.2	. . 3 ⊢ 𝐵 ∈ V
3	2	rgenw 3049	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		iunexg 7945	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
5	1, 3, 4	mp2an 692	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∈ wcel 2109  ∀wral 3045  Vcvv 3450  ∪ ciun 4958

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 2702  ax-rep 5237  ax-sep 5254  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-uni 4875  df-iun 4960

This theorem is referenced by:  tz9.1  9689  tz9.1c  9690  cplem2  9850  fseqdom  9986  pwsdompw  10163  cfsmolem  10230  ac6c4  10441  konigthlem  10528  alephreg  10542  pwfseqlem4  10622  pwfseqlem5  10623  pwxpndom2  10625  wunex2  10698  wuncval2  10707  inar1  10735  rtrclreclem1  15030  dfrtrclrec2  15031  rtrclreclem2  15032  rtrclreclem4  15034  isfunc  17833  smndex1bas  18840  smndex1sgrp  18842  smndex1mnd  18844  smndex1id  18845  dfac14  23512  txcmplem2  23536  cnextfval  23956  bnj893  34925  colinearex  36055  volsupnfl  37666  heiborlem3  37814  comptiunov2i  43702  corclrcl  43703  iunrelexpmin1  43704  trclrelexplem  43707  iunrelexpmin2  43708  dftrcl3  43716  trclfvcom  43719  cnvtrclfv  43720  cotrcltrcl  43721  trclimalb2  43722  trclfvdecomr  43724  dfrtrcl3  43729  dfrtrcl4  43734  corcltrcl  43735  cotrclrcl  43738  carageniuncllem1  46526  carageniuncllem2  46527  carageniuncl  46528  caratheodorylem1  46531  caratheodorylem2  46532  ovnovollem1  46661  ovnovollem2  46662  smfresal  46793