![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniex | Structured version Visualization version GIF version |
Description: The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3453), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
Ref | Expression |
---|---|
uniex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
uniex | ⊢ ∪ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | uniexg 7446 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Vcvv 3441 ∪ cuni 4800 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 df-ss 3898 df-uni 4801 |
This theorem is referenced by: unex 7449 iunpw 7473 elxp4 7609 elxp5 7610 1stval 7673 2ndval 7674 fo1st 7691 fo2nd 7692 cnvf1o 7789 brtpos2 7881 ixpsnf1o 8485 dffi3 8879 cnfcom2 9149 cnfcom3lem 9150 cnfcom3 9151 trcl 9154 rankc2 9284 rankxpl 9288 rankxpsuc 9295 acnlem 9459 dfac2a 9540 fin23lem14 9744 fin23lem16 9746 fin23lem17 9749 fin23lem38 9760 fin23lem39 9761 itunisuc 9830 axdc3lem2 9862 axcclem 9868 ac5b 9889 ttukey 9929 wunex2 10149 wuncval2 10158 intgru 10225 pnfex 10683 prdsval 16720 prdsds 16729 wunfunc 17161 wunnat 17218 arwval 17295 catcfuccl 17361 catcxpccl 17449 zrhval 20201 mreclatdemoBAD 21701 ptbasin2 22183 ptbasfi 22186 dfac14 22223 ptcmplem2 22658 ptcmplem3 22659 ptcmp 22663 cnextfvval 22670 cnextcn 22672 minveclem4a 24034 xrge0tsmsbi 30743 dimval 31089 dimvalfi 31090 locfinreflem 31193 pstmfval 31249 pstmxmet 31250 esumex 31398 msrval 32898 dfrdg2 33153 trpredex 33189 fvbigcup 33476 ctbssinf 34823 ptrest 35056 heiborlem1 35249 heiborlem3 35251 heibor 35259 dicval 38472 aomclem1 39998 dfac21 40010 ntrrn 40825 ntrf 40826 dssmapntrcls 40831 fourierdlem70 42818 caragendifcl 43153 cnfsmf 43374 setrec1lem3 45219 setrec2fun 45222 |
Copyright terms: Public domain | W3C validator |