![]() |
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 3054 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
4 | iunexg 7968 | . 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) | |
5 | 1, 3, 4 | mp2an 690 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ∀wral 3050 Vcvv 3461 ∪ ciun 4997 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-11 2146 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-mo 2528 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-v 3463 df-ss 3961 df-uni 4910 df-iun 4999 |
This theorem is referenced by: tz9.1 9754 tz9.1c 9755 cplem2 9915 fseqdom 10051 pwsdompw 10229 cfsmolem 10295 ac6c4 10506 konigthlem 10593 alephreg 10607 pwfseqlem4 10687 pwfseqlem5 10688 pwxpndom2 10690 wunex2 10763 wuncval2 10772 inar1 10800 rtrclreclem1 15040 dfrtrclrec2 15041 rtrclreclem2 15042 rtrclreclem4 15044 isfunc 17853 smndex1bas 18866 smndex1sgrp 18868 smndex1mnd 18870 smndex1id 18871 dfac14 23566 txcmplem2 23590 cnextfval 24010 bnj893 34690 colinearex 35787 volsupnfl 37269 heiborlem3 37417 comptiunov2i 43278 corclrcl 43279 iunrelexpmin1 43280 trclrelexplem 43283 iunrelexpmin2 43284 dftrcl3 43292 trclfvcom 43295 cnvtrclfv 43296 cotrcltrcl 43297 trclimalb2 43298 trclfvdecomr 43300 dfrtrcl3 43305 dfrtrcl4 43310 corcltrcl 43311 cotrclrcl 43314 carageniuncllem1 46047 carageniuncllem2 46048 carageniuncl 46049 caratheodorylem1 46052 caratheodorylem2 46053 ovnovollem1 46182 ovnovollem2 46183 smfresal 46314 |
Copyright terms: Public domain | W3C validator |