![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vuniex | Structured version Visualization version GIF version |
Description: The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.) |
Ref | Expression |
---|---|
vuniex | ⊢ ∪ 𝑥 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniex2 7591 | . 2 ⊢ ∃𝑦 𝑦 = ∪ 𝑥 | |
2 | 1 | issetri 3448 | 1 ⊢ ∪ 𝑥 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3432 ∪ cuni 4839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-uni 4840 |
This theorem is referenced by: uniexg 7593 uniuni 7612 rankuni 9621 r0weon 9768 dfac3 9877 dfac5lem4 9882 dfac8 9891 dfacacn 9897 kmlem2 9907 cfslb2n 10024 ttukeylem5 10269 ttukeylem6 10270 brdom7disj 10287 brdom6disj 10288 intwun 10491 wunex2 10494 fnmrc 17316 mrcfval 17317 mrisval 17339 sylow2a 19224 toprntopon 22074 distop 22145 fctop 22154 cctop 22156 ppttop 22157 epttop 22159 fncld 22173 mretopd 22243 toponmre 22244 iscnp2 22390 2ndcsep 22610 kgenf 22692 alexsubALTlem2 23199 pwsiga 32098 sigainb 32104 dmsigagen 32112 pwldsys 32125 ldsysgenld 32128 ldgenpisyslem1 32131 ddemeas 32204 brapply 34240 dfrdg4 34253 fnessref 34546 neibastop1 34548 finxpreclem2 35561 mbfresfi 35823 pwinfi 41171 pwsal 43856 intsal 43869 salexct 43873 0ome 44067 |
Copyright terms: Public domain | W3C validator |