Theorem iunex 7990

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

This proof depends on syntax axioms:   ∈ wcel 2146  ∀wral 3080  Vcvv 3454  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-11 2196  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-uni 4871  df-iun 4956

This theorem is used by:  tz9.1  9743  tz9.1c  9744  cplem2  9965  cplem2OLD  9966  fseqdom  10118  pwsdompw  10294  cfsmolem  10361  ac6c4  10572  konigthlem  10666  alephreg  10680  pwfseqlem4  10760  pwfseqlem5  10761  pwxpndom2  10763  wunex2  10836  wuncval2  10845  inar1  10873  rtrclreclem1  15225  dfrtrclrec2  15226  rtrclreclem2  15227  rtrclreclem4  15229  isfunc  18054  smndex1bas  19120  smndex1sgrp  19122  smndex1mnd  19124  smndex1id  19125  dfac14  23952  txcmplem2  23976  cnextfval  24396  bnj893  35614  ptpconn  36122  colinearex  36955  nmulprop  37069  volsupnfl  38726  dfproplem  38784  heiborlem3  38890  comptiunov2i  44849  corclrcl  44850  iunrelexpmin1  44851  trclrelexplem  44854  iunrelexpmin2  44855  dftrcl3  44863  trclfvcom  44866  cnvtrclfv  44867  cotrcltrcl  44868  trclimalb2  44869  trclfvdecomr  44871  dfrtrcl3  44876  dfrtrcl4  44881  corcltrcl  44882  cotrclrcl  44885  carageniuncllem1  47673  carageniuncllem2  47674  carageniuncl  47675  caratheodorylem1  47678  caratheodorylem2  47679  ovnovollem1  47808  ovnovollem2  47809  smfresal  47940