Theorem iunex 7903

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3436  ∪ ciun 4941

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 5218  ax-sep 5235  ax-un 7671

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 3438  df-ss 3920  df-uni 4859  df-iun 4943

This theorem is referenced by:  tz9.1  9625  tz9.1c  9626  cplem2  9786  fseqdom  9920  pwsdompw  10097  cfsmolem  10164  ac6c4  10375  konigthlem  10462  alephreg  10476  pwfseqlem4  10556  pwfseqlem5  10557  pwxpndom2  10559  wunex2  10632  wuncval2  10641  inar1  10669  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  isfunc  17771  smndex1bas  18780  smndex1sgrp  18782  smndex1mnd  18784  smndex1id  18785  dfac14  23503  txcmplem2  23527  cnextfval  23947  bnj893  34901  colinearex  36044  volsupnfl  37655  heiborlem3  37803  comptiunov2i  43689  corclrcl  43690  iunrelexpmin1  43691  trclrelexplem  43694  iunrelexpmin2  43695  dftrcl3  43703  trclfvcom  43706  cnvtrclfv  43707  cotrcltrcl  43708  trclimalb2  43709  trclfvdecomr  43711  dfrtrcl3  43716  dfrtrcl4  43721  corcltrcl  43722  cotrclrcl  43725  carageniuncllem1  46512  carageniuncllem2  46513  carageniuncl  46514  caratheodorylem1  46517  caratheodorylem2  46518  ovnovollem1  46647  ovnovollem2  46648  smfresal  46779