Theorem iunex 7912

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

Syntax hints:   ∈ wcel 2113  ∀wral 3051  Vcvv 3440  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-uni 4864  df-iun 4948

This theorem is referenced by:  tz9.1  9640  tz9.1c  9641  cplem2  9804  fseqdom  9938  pwsdompw  10115  cfsmolem  10182  ac6c4  10393  konigthlem  10481  alephreg  10495  pwfseqlem4  10575  pwfseqlem5  10576  pwxpndom2  10578  wunex2  10651  wuncval2  10660  inar1  10688  rtrclreclem1  14982  dfrtrclrec2  14983  rtrclreclem2  14984  rtrclreclem4  14986  isfunc  17790  smndex1bas  18833  smndex1sgrp  18835  smndex1mnd  18837  smndex1id  18838  dfac14  23564  txcmplem2  23588  cnextfval  24008  bnj893  35086  colinearex  36256  volsupnfl  37868  heiborlem3  38016  comptiunov2i  43968  corclrcl  43969  iunrelexpmin1  43970  trclrelexplem  43973  iunrelexpmin2  43974  dftrcl3  43982  trclfvcom  43985  cnvtrclfv  43986  cotrcltrcl  43987  trclimalb2  43988  trclfvdecomr  43990  dfrtrcl3  43995  dfrtrcl4  44000  corcltrcl  44001  cotrclrcl  44004  carageniuncllem1  46786  carageniuncllem2  46787  carageniuncl  46788  caratheodorylem1  46791  caratheodorylem2  46792  ovnovollem1  46921  ovnovollem2  46922  smfresal  47053