Theorem iunex 7951

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

Syntax hints:   ∈ wcel 2106  ∀wral 3061  Vcvv 3474  ∪ ciun 4996

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-mo 2534  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908  df-iun 4998

This theorem is referenced by:  tz9.1  9720  tz9.1c  9721  cplem2  9881  fseqdom  10017  pwsdompw  10195  cfsmolem  10261  ac6c4  10472  konigthlem  10559  alephreg  10573  pwfseqlem4  10653  pwfseqlem5  10654  pwxpndom2  10656  wunex2  10729  wuncval2  10738  inar1  10766  rtrclreclem1  15000  dfrtrclrec2  15001  rtrclreclem2  15002  rtrclreclem4  15004  isfunc  17810  smndex1bas  18783  smndex1sgrp  18785  smndex1mnd  18787  smndex1id  18788  dfac14  23113  txcmplem2  23137  cnextfval  23557  bnj893  33927  colinearex  35020  volsupnfl  36521  heiborlem3  36669  comptiunov2i  42442  corclrcl  42443  iunrelexpmin1  42444  trclrelexplem  42447  iunrelexpmin2  42448  dftrcl3  42456  trclfvcom  42459  cnvtrclfv  42460  cotrcltrcl  42461  trclimalb2  42462  trclfvdecomr  42464  dfrtrcl3  42469  dfrtrcl4  42474  corcltrcl  42475  cotrclrcl  42478  carageniuncllem1  45223  carageniuncllem2  45224  carageniuncl  45225  caratheodorylem1  45228  caratheodorylem2  45229  ovnovollem1  45358  ovnovollem2  45359  smfresal  45490