Theorem iunex 7975

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

Syntax hints:   ∈ wcel 2107  ∀wral 3050  Vcvv 3463  ∪ ciun 4971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-11 2156  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-mo 2538  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-v 3465  df-ss 3948  df-uni 4888  df-iun 4973

This theorem is referenced by:  tz9.1  9751  tz9.1c  9752  cplem2  9912  fseqdom  10048  pwsdompw  10225  cfsmolem  10292  ac6c4  10503  konigthlem  10590  alephreg  10604  pwfseqlem4  10684  pwfseqlem5  10685  pwxpndom2  10687  wunex2  10760  wuncval2  10769  inar1  10797  rtrclreclem1  15079  dfrtrclrec2  15080  rtrclreclem2  15081  rtrclreclem4  15083  isfunc  17881  smndex1bas  18889  smndex1sgrp  18891  smndex1mnd  18893  smndex1id  18894  dfac14  23573  txcmplem2  23597  cnextfval  24017  bnj893  34917  colinearex  36036  volsupnfl  37647  heiborlem3  37795  comptiunov2i  43696  corclrcl  43697  iunrelexpmin1  43698  trclrelexplem  43701  iunrelexpmin2  43702  dftrcl3  43710  trclfvcom  43713  cnvtrclfv  43714  cotrcltrcl  43715  trclimalb2  43716  trclfvdecomr  43718  dfrtrcl3  43723  dfrtrcl4  43728  corcltrcl  43729  cotrclrcl  43732  carageniuncllem1  46508  carageniuncllem2  46509  carageniuncl  46510  caratheodorylem1  46513  caratheodorylem2  46514  ovnovollem1  46643  ovnovollem2  46644  smfresal  46775