Theorem iunex 7993

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

Syntax hints:   ∈ wcel 2108  ∀wral 3061  Vcvv 3480  ∪ ciun 4991

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 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-v 3482  df-ss 3968  df-uni 4908  df-iun 4993

This theorem is referenced by:  tz9.1  9769  tz9.1c  9770  cplem2  9930  fseqdom  10066  pwsdompw  10243  cfsmolem  10310  ac6c4  10521  konigthlem  10608  alephreg  10622  pwfseqlem4  10702  pwfseqlem5  10703  pwxpndom2  10705  wunex2  10778  wuncval2  10787  inar1  10815  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  isfunc  17909  smndex1bas  18919  smndex1sgrp  18921  smndex1mnd  18923  smndex1id  18924  dfac14  23626  txcmplem2  23650  cnextfval  24070  bnj893  34942  colinearex  36061  volsupnfl  37672  heiborlem3  37820  comptiunov2i  43719  corclrcl  43720  iunrelexpmin1  43721  trclrelexplem  43724  iunrelexpmin2  43725  dftrcl3  43733  trclfvcom  43736  cnvtrclfv  43737  cotrcltrcl  43738  trclimalb2  43739  trclfvdecomr  43741  dfrtrcl3  43746  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755  carageniuncllem1  46536  carageniuncllem2  46537  carageniuncl  46538  caratheodorylem1  46541  caratheodorylem2  46542  ovnovollem1  46671  ovnovollem2  46672  smfresal  46803