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  33939  colinearex  35032  volsupnfl  36533  heiborlem3  36681  comptiunov2i  42457  corclrcl  42458  iunrelexpmin1  42459  trclrelexplem  42462  iunrelexpmin2  42463  dftrcl3  42471  trclfvcom  42474  cnvtrclfv  42475  cotrcltrcl  42476  trclimalb2  42477  trclfvdecomr  42479  dfrtrcl3  42484  dfrtrcl4  42489  corcltrcl  42490  cotrclrcl  42493  carageniuncllem1  45237  carageniuncllem2  45238  carageniuncl  45239  caratheodorylem1  45242  caratheodorylem2  45243  ovnovollem1  45372  ovnovollem2  45373  smfresal  45504