![]() |
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 7888 | . 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 2708 ax-rep 5240 ax-sep 5254 ax-un 7664 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-mo 2539 df-clab 2715 df-cleq 2729 df-clel 2815 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 9623 tz9.1c 9624 cplem2 9784 fseqdom 9920 pwsdompw 10098 cfsmolem 10164 ac6c4 10375 konigthlem 10462 alephreg 10476 pwfseqlem4 10556 pwfseqlem5 10557 pwxpndom2 10559 wunex2 10632 wuncval2 10641 inar1 10669 rtrclreclem1 14902 dfrtrclrec2 14903 rtrclreclem2 14904 rtrclreclem4 14906 isfunc 17710 smndex1bas 18676 smndex1sgrp 18678 smndex1mnd 18680 smndex1id 18681 dfac14 22921 txcmplem2 22945 cnextfval 23365 bnj893 33352 colinearex 34583 volsupnfl 36061 heiborlem3 36210 comptiunov2i 41889 corclrcl 41890 iunrelexpmin1 41891 trclrelexplem 41894 iunrelexpmin2 41895 dftrcl3 41903 trclfvcom 41906 cnvtrclfv 41907 cotrcltrcl 41908 trclimalb2 41909 trclfvdecomr 41911 dfrtrcl3 41916 dfrtrcl4 41921 corcltrcl 41922 cotrclrcl 41925 carageniuncllem1 44663 carageniuncllem2 44664 carageniuncl 44665 caratheodorylem1 44668 caratheodorylem2 44669 ovnovollem1 44798 ovnovollem2 44799 smfresal 44930 |
Copyright terms: Public domain | W3C validator |