Theorem iunex 7950

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

Syntax hints:   ∈ wcel 2143  ∀wral 3077  Vcvv 3455  ∪ ciun 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-v 3457  df-ss 3922  df-uni 4867  df-iun 4952

This theorem is referenced by:  tz9.1  9685  tz9.1c  9686  cplem2  9849  fseqdom  9983  pwsdompw  10160  cfsmolem  10228  ac6c4  10439  konigthlem  10527  alephreg  10541  pwfseqlem4  10621  pwfseqlem5  10622  pwxpndom2  10624  wunex2  10697  wuncval2  10706  inar1  10734  rtrclreclem1  15071  dfrtrclrec2  15072  rtrclreclem2  15073  rtrclreclem4  15075  isfunc  17898  smndex1bas  18944  smndex1sgrp  18946  smndex1mnd  18948  smndex1id  18949  dfac14  23679  txcmplem2  23703  cnextfval  24123  bnj893  35224  colinearex  36411  nmulprop  36541  volsupnfl  38165  heiborlem3  38313  comptiunov2i  44283  corclrcl  44284  iunrelexpmin1  44285  trclrelexplem  44288  iunrelexpmin2  44289  dftrcl3  44297  trclfvcom  44300  cnvtrclfv  44301  cotrcltrcl  44302  trclimalb2  44303  trclfvdecomr  44305  dfrtrcl3  44310  dfrtrcl4  44315  corcltrcl  44316  cotrclrcl  44319  carageniuncllem1  47096  carageniuncllem2  47097  carageniuncl  47098  caratheodorylem1  47101  caratheodorylem2  47102  ovnovollem1  47231  ovnovollem2  47232  smfresal  47363