Theorem iunex 7922

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

Syntax hints:   ∈ wcel 2114  ∀wral 3052  Vcvv 3442  ∪ ciun 4948

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 2709  ax-rep 5226  ax-sep 5243  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-ss 3920  df-uni 4866  df-iun 4950

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  14992  dfrtrclrec2  14993  rtrclreclem2  14994  rtrclreclem4  14996  isfunc  17800  smndex1bas  18846  smndex1sgrp  18848  smndex1mnd  18850  smndex1id  18851  dfac14  23577  txcmplem2  23601  cnextfval  24021  bnj893  35108  colinearex  36280  volsupnfl  37920  heiborlem3  38068  comptiunov2i  44066  corclrcl  44067  iunrelexpmin1  44068  trclrelexplem  44071  iunrelexpmin2  44072  dftrcl3  44080  trclfvcom  44083  cnvtrclfv  44084  cotrcltrcl  44085  trclimalb2  44086  trclfvdecomr  44088  dfrtrcl3  44093  dfrtrcl4  44098  corcltrcl  44099  cotrclrcl  44102  carageniuncllem1  46883  carageniuncllem2  46884  carageniuncl  46885  caratheodorylem1  46888  caratheodorylem2  46889  ovnovollem1  47018  ovnovollem2  47019  smfresal  47150