Theorem iunex 7926

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3444  ∪ ciun 4951

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 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3446  df-ss 3928  df-uni 4868  df-iun 4953

This theorem is referenced by:  tz9.1  9658  tz9.1c  9659  cplem2  9819  fseqdom  9955  pwsdompw  10132  cfsmolem  10199  ac6c4  10410  konigthlem  10497  alephreg  10511  pwfseqlem4  10591  pwfseqlem5  10592  pwxpndom2  10594  wunex2  10667  wuncval2  10676  inar1  10704  rtrclreclem1  14999  dfrtrclrec2  15000  rtrclreclem2  15001  rtrclreclem4  15003  isfunc  17806  smndex1bas  18815  smndex1sgrp  18817  smndex1mnd  18819  smndex1id  18820  dfac14  23538  txcmplem2  23562  cnextfval  23982  bnj893  34911  colinearex  36041  volsupnfl  37652  heiborlem3  37800  comptiunov2i  43688  corclrcl  43689  iunrelexpmin1  43690  trclrelexplem  43693  iunrelexpmin2  43694  dftrcl3  43702  trclfvcom  43705  cnvtrclfv  43706  cotrcltrcl  43707  trclimalb2  43708  trclfvdecomr  43710  dfrtrcl3  43715  dfrtrcl4  43720  corcltrcl  43721  cotrclrcl  43724  carageniuncllem1  46512  carageniuncllem2  46513  carageniuncl  46514  caratheodorylem1  46517  caratheodorylem2  46518  ovnovollem1  46647  ovnovollem2  46648  smfresal  46779