Theorem iunex 7017

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

Syntax hints:   ∈ wcel 1977  ∀wral 2896  Vcvv 3173  ∪ ciun 4450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pr 4828  ax-un 6825

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798

This theorem is referenced by:  abrexex2  7018  tz9.1  8466  tz9.1c  8467  cplem2  8614  fseqdom  8710  pwsdompw  8887  cfsmolem  8953  ac6c4  9164  konigthlem  9247  alephreg  9261  pwfseqlem4  9341  pwfseqlem5  9342  pwxpndom2  9344  wunex2  9417  wuncval2  9426  inar1  9454  dfrtrclrec2  13594  rtrclreclem1  13595  rtrclreclem2  13596  rtrclreclem4  13598  isfunc  16296  dfac14  21179  txcmplem2  21203  cnextfval  21624  bnj893  30046  colinearex  31131  volsupnfl  32418  heiborlem3  32576  comptiunov2i  36811  corclrcl  36812  iunrelexpmin1  36813  trclrelexplem  36816  iunrelexpmin2  36817  dftrcl3  36825  trclfvcom  36828  cnvtrclfv  36829  cotrcltrcl  36830  trclimalb2  36831  trclfvdecomr  36833  dfrtrcl3  36838  dfrtrcl4  36843  corcltrcl  36844  cotrclrcl  36847  carageniuncllem1  39205  carageniuncllem2  39206  carageniuncl  39207  caratheodorylem1  39210  caratheodorylem2  39211  ovnovollem1  39340  ovnovollem2  39341  smfresal  39467