![]() |
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.) |
Ref | Expression |
---|---|
vuniex | ⊢ ∪ 𝑥 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3440 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | uniex 7323 | 1 ⊢ ∪ 𝑥 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 Vcvv 3437 ∪ cuni 4745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-sep 5094 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rex 3111 df-v 3439 df-uni 4746 |
This theorem is referenced by: uniexg 7325 uniuni 7341 rankuni 9138 r0weon 9284 dfac3 9393 dfac5lem4 9398 dfac8 9407 dfacacn 9413 kmlem2 9423 cfslb2n 9536 ttukeylem5 9781 ttukeylem6 9782 brdom7disj 9799 brdom6disj 9800 intwun 10003 wunex2 10006 fnmrc 16707 mrcfval 16708 mrisval 16730 sylow2a 18474 toprntopon 21217 distop 21287 fctop 21296 cctop 21298 ppttop 21299 epttop 21301 fncld 21314 mretopd 21384 toponmre 21385 iscnp2 21531 2ndcsep 21751 kgenf 21833 alexsubALTlem2 22340 pwsiga 31006 sigainb 31012 dmsigagen 31020 pwldsys 31033 ldsysgenld 31036 ldgenpisyslem1 31039 ddemeas 31112 brapply 33009 dfrdg4 33022 fnessref 33315 neibastop1 33317 finxpreclem2 34221 mbfresfi 34488 pwinfi 39427 pwsal 42162 intsal 42175 salexct 42179 0ome 42373 |
Copyright terms: Public domain | W3C validator |