![]() |
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 7721 | . 2 ⊢ ∃𝑦 𝑦 = ∪ 𝑥 | |
2 | 1 | issetri 3483 | 1 ⊢ ∪ 𝑥 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 Vcvv 3466 ∪ cuni 4899 |
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-ext 2695 ax-sep 5289 ax-un 7718 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-uni 4900 |
This theorem is referenced by: uniexg 7723 uniuni 7742 rankuni 9854 r0weon 10003 dfac3 10112 dfac5lem4 10117 dfac8 10126 dfacacn 10132 kmlem2 10142 cfslb2n 10259 ttukeylem5 10504 ttukeylem6 10505 brdom7disj 10522 brdom6disj 10523 intwun 10726 wunex2 10729 fnmrc 17550 mrcfval 17551 mrisval 17573 sylow2a 19529 toprntopon 22749 distop 22820 fctop 22829 cctop 22831 ppttop 22832 epttop 22834 fncld 22848 mretopd 22918 toponmre 22919 iscnp2 23065 2ndcsep 23285 kgenf 23367 alexsubALTlem2 23874 pwsiga 33617 sigainb 33623 dmsigagen 33631 pwldsys 33644 ldsysgenld 33647 ldgenpisyslem1 33650 ddemeas 33723 brapply 35405 dfrdg4 35418 fnessref 35732 neibastop1 35734 finxpreclem2 36761 mbfresfi 37024 pwinfi 42804 pwsal 45516 intsal 45531 salexct 45535 0ome 45730 |
Copyright terms: Public domain | W3C validator |