Theorem iunex 7947

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

Syntax hints:   ∈ wcel 2109  ∀wral 3044  Vcvv 3447  ∪ ciun 4955

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 5234  ax-sep 5251  ax-un 7711

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 3449  df-ss 3931  df-uni 4872  df-iun 4957

This theorem is referenced by:  tz9.1  9682  tz9.1c  9683  cplem2  9843  fseqdom  9979  pwsdompw  10156  cfsmolem  10223  ac6c4  10434  konigthlem  10521  alephreg  10535  pwfseqlem4  10615  pwfseqlem5  10616  pwxpndom2  10618  wunex2  10691  wuncval2  10700  inar1  10728  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  isfunc  17826  smndex1bas  18833  smndex1sgrp  18835  smndex1mnd  18837  smndex1id  18838  dfac14  23505  txcmplem2  23529  cnextfval  23949  bnj893  34918  colinearex  36048  volsupnfl  37659  heiborlem3  37807  comptiunov2i  43695  corclrcl  43696  iunrelexpmin1  43697  trclrelexplem  43700  iunrelexpmin2  43701  dftrcl3  43709  trclfvcom  43712  cnvtrclfv  43713  cotrcltrcl  43714  trclimalb2  43715  trclfvdecomr  43717  dfrtrcl3  43722  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  carageniuncllem1  46519  carageniuncllem2  46520  carageniuncl  46521  caratheodorylem1  46524  caratheodorylem2  46525  ovnovollem1  46654  ovnovollem2  46655  smfresal  46786