Theorem iunex 7967

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

Syntax hints:   ∈ wcel 2108  ∀wral 3051  Vcvv 3459  ∪ ciun 4967

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 2707  ax-rep 5249  ax-sep 5266  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-uni 4884  df-iun 4969

This theorem is referenced by:  tz9.1  9743  tz9.1c  9744  cplem2  9904  fseqdom  10040  pwsdompw  10217  cfsmolem  10284  ac6c4  10495  konigthlem  10582  alephreg  10596  pwfseqlem4  10676  pwfseqlem5  10677  pwxpndom2  10679  wunex2  10752  wuncval2  10761  inar1  10789  rtrclreclem1  15076  dfrtrclrec2  15077  rtrclreclem2  15078  rtrclreclem4  15080  isfunc  17877  smndex1bas  18884  smndex1sgrp  18886  smndex1mnd  18888  smndex1id  18889  dfac14  23556  txcmplem2  23580  cnextfval  24000  bnj893  34959  colinearex  36078  volsupnfl  37689  heiborlem3  37837  comptiunov2i  43730  corclrcl  43731  iunrelexpmin1  43732  trclrelexplem  43735  iunrelexpmin2  43736  dftrcl3  43744  trclfvcom  43747  cnvtrclfv  43748  cotrcltrcl  43749  trclimalb2  43750  trclfvdecomr  43752  dfrtrcl3  43757  dfrtrcl4  43762  corcltrcl  43763  cotrclrcl  43766  carageniuncllem1  46550  carageniuncllem2  46551  carageniuncl  46552  caratheodorylem1  46555  caratheodorylem2  46556  ovnovollem1  46685  ovnovollem2  46686  smfresal  46817