Theorem iunex 7911

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

Syntax hints:   ∈ wcel 2119  ∀wral 3053  Vcvv 3431  ∪ ciun 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-ext 2711  ax-rep 5200  ax-sep 5219  ax-un 7679

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-uni 4840  df-iun 4924

This theorem is referenced by:  tz9.1  9642  tz9.1c  9643  cplem2  9806  fseqdom  9940  pwsdompw  10117  cfsmolem  10184  ac6c4  10395  konigthlem  10483  alephreg  10497  pwfseqlem4  10577  pwfseqlem5  10578  pwxpndom2  10580  wunex2  10653  wuncval2  10662  inar1  10690  rtrclreclem1  15011  dfrtrclrec2  15012  rtrclreclem2  15013  rtrclreclem4  15015  isfunc  17823  smndex1bas  18869  smndex1sgrp  18871  smndex1mnd  18873  smndex1id  18874  dfac14  23602  txcmplem2  23626  cnextfval  24046  bnj893  35119  colinearex  36297  volsupnfl  38041  heiborlem3  38189  comptiunov2i  44159  corclrcl  44160  iunrelexpmin1  44161  trclrelexplem  44164  iunrelexpmin2  44165  dftrcl3  44173  trclfvcom  44176  cnvtrclfv  44177  cotrcltrcl  44178  trclimalb2  44179  trclfvdecomr  44181  dfrtrcl3  44186  dfrtrcl4  44191  corcltrcl  44192  cotrclrcl  44195  carageniuncllem1  46972  carageniuncllem2  46973  carageniuncl  46974  caratheodorylem1  46977  caratheodorylem2  46978  ovnovollem1  47107  ovnovollem2  47108  smfresal  47239