Theorem iunex 7921

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

Syntax hints:   ∈ wcel 2114  ∀wral 3051  Vcvv 3429  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-uni 4851  df-iun 4935

This theorem is referenced by:  tz9.1  9650  tz9.1c  9651  cplem2  9814  fseqdom  9948  pwsdompw  10125  cfsmolem  10192  ac6c4  10403  konigthlem  10491  alephreg  10505  pwfseqlem4  10585  pwfseqlem5  10586  pwxpndom2  10588  wunex2  10661  wuncval2  10670  inar1  10698  rtrclreclem1  15019  dfrtrclrec2  15020  rtrclreclem2  15021  rtrclreclem4  15023  isfunc  17831  smndex1bas  18877  smndex1sgrp  18879  smndex1mnd  18881  smndex1id  18882  dfac14  23583  txcmplem2  23607  cnextfval  24027  bnj893  35070  colinearex  36242  volsupnfl  37986  heiborlem3  38134  comptiunov2i  44133  corclrcl  44134  iunrelexpmin1  44135  trclrelexplem  44138  iunrelexpmin2  44139  dftrcl3  44147  trclfvcom  44150  cnvtrclfv  44151  cotrcltrcl  44152  trclimalb2  44153  trclfvdecomr  44155  dfrtrcl3  44160  dfrtrcl4  44165  corcltrcl  44166  cotrclrcl  44169  carageniuncllem1  46949  carageniuncllem2  46950  carageniuncl  46951  caratheodorylem1  46954  caratheodorylem2  46955  ovnovollem1  47084  ovnovollem2  47085  smfresal  47216