Theorem iunex 7961

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

Syntax hints:   ∈ wcel 2143  ∀wral 3079  Vcvv 3455  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-uni 4873  df-iun 4958

This theorem is referenced by:  tz9.1  9694  tz9.1c  9695  cplem2  9872  fseqdom  10006  pwsdompw  10182  cfsmolem  10249  ac6c4  10460  konigthlem  10548  alephreg  10562  pwfseqlem4  10642  pwfseqlem5  10643  pwxpndom2  10645  wunex2  10718  wuncval2  10727  inar1  10755  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  isfunc  17916  smndex1bas  18963  smndex1sgrp  18965  smndex1mnd  18967  smndex1id  18968  dfac14  23775  txcmplem2  23799  cnextfval  24219  bnj893  35316  colinearex  36552  nmulprop  36682  volsupnfl  38336  heiborlem3  38484  comptiunov2i  44452  corclrcl  44453  iunrelexpmin1  44454  trclrelexplem  44457  iunrelexpmin2  44458  dftrcl3  44466  trclfvcom  44469  cnvtrclfv  44470  cotrcltrcl  44471  trclimalb2  44472  trclfvdecomr  44474  dfrtrcl3  44479  dfrtrcl4  44484  corcltrcl  44485  cotrclrcl  44488  carageniuncllem1  47255  carageniuncllem2  47256  carageniuncl  47257  caratheodorylem1  47260  caratheodorylem2  47261  ovnovollem1  47390  ovnovollem2  47391  smfresal  47522