Theorem iunex 7955

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

Syntax hints:   ∈ wcel 2107  ∀wral 3062  Vcvv 3475  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-mo 2535  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-iun 5000

This theorem is referenced by:  tz9.1  9724  tz9.1c  9725  cplem2  9885  fseqdom  10021  pwsdompw  10199  cfsmolem  10265  ac6c4  10476  konigthlem  10563  alephreg  10577  pwfseqlem4  10657  pwfseqlem5  10658  pwxpndom2  10660  wunex2  10733  wuncval2  10742  inar1  10770  rtrclreclem1  15004  dfrtrclrec2  15005  rtrclreclem2  15006  rtrclreclem4  15008  isfunc  17814  smndex1bas  18787  smndex1sgrp  18789  smndex1mnd  18791  smndex1id  18792  dfac14  23122  txcmplem2  23146  cnextfval  23566  bnj893  33970  colinearex  35063  volsupnfl  36581  heiborlem3  36729  comptiunov2i  42505  corclrcl  42506  iunrelexpmin1  42507  trclrelexplem  42510  iunrelexpmin2  42511  dftrcl3  42519  trclfvcom  42522  cnvtrclfv  42523  cotrcltrcl  42524  trclimalb2  42525  trclfvdecomr  42527  dfrtrcl3  42532  dfrtrcl4  42537  corcltrcl  42538  cotrclrcl  42541  carageniuncllem1  45285  carageniuncllem2  45286  carageniuncl  45287  caratheodorylem1  45290  caratheodorylem2  45291  ovnovollem1  45420  ovnovollem2  45421  smfresal  45552