Theorem iunex 7811

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 3076	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		iunexg 7806	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
5	1, 3, 4	mp2an 689	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∈ wcel 2106  ∀wral 3064  Vcvv 3432  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-iun 4926

This theorem is referenced by:  tz9.1  9487  tz9.1c  9488  cplem2  9648  fseqdom  9782  pwsdompw  9960  cfsmolem  10026  ac6c4  10237  konigthlem  10324  alephreg  10338  pwfseqlem4  10418  pwfseqlem5  10419  pwxpndom2  10421  wunex2  10494  wuncval2  10503  inar1  10531  rtrclreclem1  14768  dfrtrclrec2  14769  rtrclreclem2  14770  rtrclreclem4  14772  isfunc  17579  smndex1bas  18545  smndex1sgrp  18547  smndex1mnd  18549  smndex1id  18550  dfac14  22769  txcmplem2  22793  cnextfval  23213  bnj893  32908  colinearex  34362  volsupnfl  35822  heiborlem3  35971  comptiunov2i  41314  corclrcl  41315  iunrelexpmin1  41316  trclrelexplem  41319  iunrelexpmin2  41320  dftrcl3  41328  trclfvcom  41331  cnvtrclfv  41332  cotrcltrcl  41333  trclimalb2  41334  trclfvdecomr  41336  dfrtrcl3  41341  dfrtrcl4  41346  corcltrcl  41347  cotrclrcl  41350  carageniuncllem1  44059  carageniuncllem2  44060  carageniuncl  44061  caratheodorylem1  44064  caratheodorylem2  44065  ovnovollem1  44194  ovnovollem2  44195  smfresal  44322