Theorem iunex 7910

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

Syntax hints:   ∈ wcel 2113  ∀wral 3049  Vcvv 3438  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-uni 4862  df-iun 4946

This theorem is referenced by:  tz9.1  9636  tz9.1c  9637  cplem2  9800  fseqdom  9934  pwsdompw  10111  cfsmolem  10178  ac6c4  10389  konigthlem  10477  alephreg  10491  pwfseqlem4  10571  pwfseqlem5  10572  pwxpndom2  10574  wunex2  10647  wuncval2  10656  inar1  10684  rtrclreclem1  14978  dfrtrclrec2  14979  rtrclreclem2  14980  rtrclreclem4  14982  isfunc  17786  smndex1bas  18829  smndex1sgrp  18831  smndex1mnd  18833  smndex1id  18834  dfac14  23560  txcmplem2  23584  cnextfval  24004  bnj893  35033  colinearex  36203  volsupnfl  37805  heiborlem3  37953  comptiunov2i  43889  corclrcl  43890  iunrelexpmin1  43891  trclrelexplem  43894  iunrelexpmin2  43895  dftrcl3  43903  trclfvcom  43906  cnvtrclfv  43907  cotrcltrcl  43908  trclimalb2  43909  trclfvdecomr  43911  dfrtrcl3  43916  dfrtrcl4  43921  corcltrcl  43922  cotrclrcl  43925  carageniuncllem1  46707  carageniuncllem2  46708  carageniuncl  46709  caratheodorylem1  46712  caratheodorylem2  46713  ovnovollem1  46842  ovnovollem2  46843  smfresal  46974