Theorem iunex 7900

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

Syntax hints:   ∈ wcel 2111  ∀wral 3047  Vcvv 3436  ∪ ciun 4939

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 2113  ax-9 2121  ax-11 2160  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-v 3438  df-ss 3914  df-uni 4857  df-iun 4941

This theorem is referenced by:  tz9.1  9619  tz9.1c  9620  cplem2  9783  fseqdom  9917  pwsdompw  10094  cfsmolem  10161  ac6c4  10372  konigthlem  10459  alephreg  10473  pwfseqlem4  10553  pwfseqlem5  10554  pwxpndom2  10556  wunex2  10629  wuncval2  10638  inar1  10666  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  isfunc  17771  smndex1bas  18814  smndex1sgrp  18816  smndex1mnd  18818  smndex1id  18819  dfac14  23533  txcmplem2  23557  cnextfval  23977  bnj893  34940  colinearex  36104  volsupnfl  37715  heiborlem3  37863  comptiunov2i  43809  corclrcl  43810  iunrelexpmin1  43811  trclrelexplem  43814  iunrelexpmin2  43815  dftrcl3  43823  trclfvcom  43826  cnvtrclfv  43827  cotrcltrcl  43828  trclimalb2  43829  trclfvdecomr  43831  dfrtrcl3  43836  dfrtrcl4  43841  corcltrcl  43842  cotrclrcl  43845  carageniuncllem1  46629  carageniuncllem2  46630  carageniuncl  46631  caratheodorylem1  46634  caratheodorylem2  46635  ovnovollem1  46764  ovnovollem2  46765  smfresal  46896