Theorem iunex 8009

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

Syntax hints:   ∈ wcel 2108  ∀wral 3067  Vcvv 3488  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2158  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-mo 2543  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-uni 4932  df-iun 5017

This theorem is referenced by:  tz9.1  9798  tz9.1c  9799  cplem2  9959  fseqdom  10095  pwsdompw  10272  cfsmolem  10339  ac6c4  10550  konigthlem  10637  alephreg  10651  pwfseqlem4  10731  pwfseqlem5  10732  pwxpndom2  10734  wunex2  10807  wuncval2  10816  inar1  10844  rtrclreclem1  15106  dfrtrclrec2  15107  rtrclreclem2  15108  rtrclreclem4  15110  isfunc  17928  smndex1bas  18941  smndex1sgrp  18943  smndex1mnd  18945  smndex1id  18946  dfac14  23647  txcmplem2  23671  cnextfval  24091  bnj893  34904  colinearex  36024  volsupnfl  37625  heiborlem3  37773  comptiunov2i  43668  corclrcl  43669  iunrelexpmin1  43670  trclrelexplem  43673  iunrelexpmin2  43674  dftrcl3  43682  trclfvcom  43685  cnvtrclfv  43686  cotrcltrcl  43687  trclimalb2  43688  trclfvdecomr  43690  dfrtrcl3  43695  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704  carageniuncllem1  46442  carageniuncllem2  46443  carageniuncl  46444  caratheodorylem1  46447  caratheodorylem2  46448  ovnovollem1  46577  ovnovollem2  46578  smfresal  46709