Theorem iunex 7966

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

This proof depends on syntax axioms:   ∈ wcel 2145  ∀wral 3076  Vcvv 3450  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-uni 4868  df-iun 4953

This theorem is used by:  tz9.1  9711  tz9.1c  9712  cplem2  9894  cplem2OLD  9895  fseqdom  10032  pwsdompw  10208  cfsmolem  10275  ac6c4  10486  konigthlem  10580  alephreg  10594  pwfseqlem4  10674  pwfseqlem5  10675  pwxpndom2  10677  wunex2  10750  wuncval2  10759  inar1  10787  rtrclreclem1  15133  dfrtrclrec2  15134  rtrclreclem2  15135  rtrclreclem4  15137  isfunc  17956  smndex1bas  19021  smndex1sgrp  19023  smndex1mnd  19025  smndex1id  19026  dfac14  23847  txcmplem2  23871  cnextfval  24291  bnj893  35440  colinearex  36643  nmulprop  36773  volsupnfl  38417  heiborlem3  38566  comptiunov2i  44549  corclrcl  44550  iunrelexpmin1  44551  trclrelexplem  44554  iunrelexpmin2  44555  dftrcl3  44563  trclfvcom  44566  cnvtrclfv  44567  cotrcltrcl  44568  trclimalb2  44569  trclfvdecomr  44571  dfrtrcl3  44576  dfrtrcl4  44581  corcltrcl  44582  cotrclrcl  44585  carageniuncllem1  47352  carageniuncllem2  47353  carageniuncl  47354  caratheodorylem1  47357  caratheodorylem2  47358  ovnovollem1  47487  ovnovollem2  47488  smfresal  47619