Theorem iunex 7971

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

This proof depends on syntax axioms:   ∈ wcel 2146  ∀wral 3081  Vcvv 3457  ∪ ciun 4958

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 2148  ax-9 2156  ax-11 2195  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-uni 4875  df-iun 4960

This theorem is used by:  tz9.1  9705  tz9.1c  9706  cplem2  9888  cplem2OLD  9889  fseqdom  10026  pwsdompw  10202  cfsmolem  10269  ac6c4  10480  konigthlem  10570  alephreg  10584  pwfseqlem4  10664  pwfseqlem5  10665  pwxpndom2  10667  wunex2  10740  wuncval2  10749  inar1  10777  rtrclreclem1  15120  dfrtrclrec2  15121  rtrclreclem2  15122  rtrclreclem4  15124  isfunc  17945  smndex1bas  19007  smndex1sgrp  19009  smndex1mnd  19011  smndex1id  19012  dfac14  23828  txcmplem2  23852  cnextfval  24272  bnj893  35383  colinearex  36591  nmulprop  36721  volsupnfl  38375  heiborlem3  38524  comptiunov2i  44492  corclrcl  44493  iunrelexpmin1  44494  trclrelexplem  44497  iunrelexpmin2  44498  dftrcl3  44506  trclfvcom  44509  cnvtrclfv  44510  cotrcltrcl  44511  trclimalb2  44512  trclfvdecomr  44514  dfrtrcl3  44519  dfrtrcl4  44524  corcltrcl  44525  cotrclrcl  44528  carageniuncllem1  47295  carageniuncllem2  47296  carageniuncl  47297  caratheodorylem1  47300  caratheodorylem2  47301  ovnovollem1  47430  ovnovollem2  47431  smfresal  47562