Theorem iunex 7992

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

Syntax hints:   ∈ wcel 2106  ∀wral 3059  Vcvv 3478  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-mo 2538  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-ss 3980  df-uni 4913  df-iun 4998

This theorem is referenced by:  tz9.1  9767  tz9.1c  9768  cplem2  9928  fseqdom  10064  pwsdompw  10241  cfsmolem  10308  ac6c4  10519  konigthlem  10606  alephreg  10620  pwfseqlem4  10700  pwfseqlem5  10701  pwxpndom2  10703  wunex2  10776  wuncval2  10785  inar1  10813  rtrclreclem1  15093  dfrtrclrec2  15094  rtrclreclem2  15095  rtrclreclem4  15097  isfunc  17915  smndex1bas  18932  smndex1sgrp  18934  smndex1mnd  18936  smndex1id  18937  dfac14  23642  txcmplem2  23666  cnextfval  24086  bnj893  34921  colinearex  36042  volsupnfl  37652  heiborlem3  37800  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  46477  carageniuncllem2  46478  carageniuncl  46479  caratheodorylem1  46482  caratheodorylem2  46483  ovnovollem1  46612  ovnovollem2  46613  smfresal  46744