Theorem iunex 7915

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

Syntax hints:   ∈ wcel 2114  ∀wral 3052  Vcvv 3430  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-uni 4852  df-iun 4936

This theorem is referenced by:  tz9.1  9644  tz9.1c  9645  cplem2  9808  fseqdom  9942  pwsdompw  10119  cfsmolem  10186  ac6c4  10397  konigthlem  10485  alephreg  10499  pwfseqlem4  10579  pwfseqlem5  10580  pwxpndom2  10582  wunex2  10655  wuncval2  10664  inar1  10692  rtrclreclem1  15013  dfrtrclrec2  15014  rtrclreclem2  15015  rtrclreclem4  15017  isfunc  17825  smndex1bas  18871  smndex1sgrp  18873  smndex1mnd  18875  smndex1id  18876  dfac14  23596  txcmplem2  23620  cnextfval  24040  bnj893  35089  colinearex  36261  volsupnfl  38003  heiborlem3  38151  comptiunov2i  44154  corclrcl  44155  iunrelexpmin1  44156  trclrelexplem  44159  iunrelexpmin2  44160  dftrcl3  44168  trclfvcom  44171  cnvtrclfv  44172  cotrcltrcl  44173  trclimalb2  44174  trclfvdecomr  44176  dfrtrcl3  44181  dfrtrcl4  44186  corcltrcl  44187  cotrclrcl  44190  carageniuncllem1  46970  carageniuncllem2  46971  carageniuncl  46972  caratheodorylem1  46975  caratheodorylem2  46976  ovnovollem1  47105  ovnovollem2  47106  smfresal  47237