Theorem iunex 7965

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

Syntax hints:   ∈ wcel 2149  ∀wral 3085  Vcvv 3463  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-11 2198  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-mo 2573  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-uni 4877  df-iun 4962

This theorem is referenced by:  tz9.1  9698  tz9.1c  9699  cplem2  9876  fseqdom  10010  pwsdompw  10186  cfsmolem  10254  ac6c4  10465  konigthlem  10553  alephreg  10567  pwfseqlem4  10647  pwfseqlem5  10648  pwxpndom2  10650  wunex2  10723  wuncval2  10732  inar1  10760  rtrclreclem1  15094  dfrtrclrec2  15095  rtrclreclem2  15096  rtrclreclem4  15098  isfunc  17921  smndex1bas  18968  smndex1sgrp  18970  smndex1mnd  18972  smndex1id  18973  dfac14  23744  txcmplem2  23768  cnextfval  24188  bnj893  35261  colinearex  36485  nmulprop  36615  volsupnfl  38238  heiborlem3  38386  comptiunov2i  44358  corclrcl  44359  iunrelexpmin1  44360  trclrelexplem  44363  iunrelexpmin2  44364  dftrcl3  44372  trclfvcom  44375  cnvtrclfv  44376  cotrcltrcl  44377  trclimalb2  44378  trclfvdecomr  44380  dfrtrcl3  44385  dfrtrcl4  44390  corcltrcl  44391  cotrclrcl  44394  carageniuncllem1  47161  carageniuncllem2  47162  carageniuncl  47163  caratheodorylem1  47166  caratheodorylem2  47167  ovnovollem1  47296  ovnovollem2  47297  smfresal  47428