![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunex | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
iunex.1 | ⊢ 𝐴 ∈ V |
iunex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
iunex | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | iunex.2 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 2 | rgenw 3066 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
4 | iunexg 7892 | . 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | |
5 | 1, 3, 4 | mp2an 690 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ∀wral 3062 Vcvv 3443 ∪ ciun 4952 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2707 ax-rep 5240 ax-sep 5254 ax-un 7668 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-mo 2538 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-rex 3072 df-v 3445 df-in 3915 df-ss 3925 df-uni 4864 df-iun 4954 |
This theorem is referenced by: tz9.1 9661 tz9.1c 9662 cplem2 9822 fseqdom 9958 pwsdompw 10136 cfsmolem 10202 ac6c4 10413 konigthlem 10500 alephreg 10514 pwfseqlem4 10594 pwfseqlem5 10595 pwxpndom2 10597 wunex2 10670 wuncval2 10679 inar1 10707 rtrclreclem1 14934 dfrtrclrec2 14935 rtrclreclem2 14936 rtrclreclem4 14938 isfunc 17742 smndex1bas 18708 smndex1sgrp 18710 smndex1mnd 18712 smndex1id 18713 dfac14 22953 txcmplem2 22977 cnextfval 23397 bnj893 33409 colinearex 34612 volsupnfl 36090 heiborlem3 36239 comptiunov2i 41920 corclrcl 41921 iunrelexpmin1 41922 trclrelexplem 41925 iunrelexpmin2 41926 dftrcl3 41934 trclfvcom 41937 cnvtrclfv 41938 cotrcltrcl 41939 trclimalb2 41940 trclfvdecomr 41942 dfrtrcl3 41947 dfrtrcl4 41952 corcltrcl 41953 cotrclrcl 41956 carageniuncllem1 44694 carageniuncllem2 44695 carageniuncl 44696 caratheodorylem1 44699 caratheodorylem2 44700 ovnovollem1 44829 ovnovollem2 44830 smfresal 44961 |
Copyright terms: Public domain | W3C validator |