Theorem iunex 7980

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3077  Vcvv 3451  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-uni 4868  df-iun 4953

This theorem is used by:  tz9.1  9730  tz9.1c  9731  cplem2  9952  cplem2OLD  9953  fseqdom  10105  pwsdompw  10281  cfsmolem  10348  ac6c4  10559  konigthlem  10653  alephreg  10667  pwfseqlem4  10747  pwfseqlem5  10748  pwxpndom2  10750  wunex2  10823  wuncval2  10832  inar1  10860  rtrclreclem1  15210  dfrtrclrec2  15211  rtrclreclem2  15212  rtrclreclem4  15214  isfunc  18039  smndex1bas  19105  smndex1sgrp  19107  smndex1mnd  19109  smndex1id  19110  dfac14  23937  txcmplem2  23961  cnextfval  24381  bnj893  35558  colinearex  36825  nmulprop  36939  volsupnfl  38583  dfproplem  38641  heiborlem3  38747  comptiunov2i  44705  corclrcl  44706  iunrelexpmin1  44707  trclrelexplem  44710  iunrelexpmin2  44711  dftrcl3  44719  trclfvcom  44722  cnvtrclfv  44723  cotrcltrcl  44724  trclimalb2  44725  trclfvdecomr  44727  dfrtrcl3  44732  dfrtrcl4  44737  corcltrcl  44738  cotrclrcl  44741  carageniuncllem1  47530  carageniuncllem2  47531  carageniuncl  47532  caratheodorylem1  47535  caratheodorylem2  47536  ovnovollem1  47665  ovnovollem2  47666  smfresal  47797