| 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 3494), 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 7760 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: unexOLD 7765 iunpw 7791 elxp4 7944 elxp5 7945 1stval 8016 2ndval 8017 fo1st 8034 fo2nd 8035 cnvf1o 8136 brtpos2 8257 naddcllem 8714 ixpsnf1o 8978 dffi3 9471 cnfcom2 9742 cnfcom3lem 9743 cnfcom3 9744 ttrclse 9767 trcl 9768 rankc2 9911 rankxpl 9915 rankxpsuc 9922 acnlem 10088 dfac2a 10170 fin23lem14 10373 fin23lem16 10375 fin23lem17 10378 fin23lem38 10389 fin23lem39 10390 itunisuc 10459 axdc3lem2 10491 axcclem 10497 ac5b 10518 ttukey 10558 wunex2 10778 wuncval2 10787 intgru 10854 pnfex 11314 prdsvallem 17499 prdsval 17500 prdsds 17509 wunfunc 17946 wunnat 18004 arwval 18088 catcfuccl 18163 catcxpccl 18252 zrhval 21518 mreclatdemoBAD 23104 ptbasin2 23586 ptbasfi 23589 dfac14 23626 ptcmplem2 24061 ptcmplem3 24062 ptcmp 24066 cnextfvval 24073 cnextcn 24075 minveclem4a 25464 oldf 27896 madefi 27950 precsexlem10 28240 xrge0tsmsbi 33066 dimval 33651 dimvalfi 33652 locfinreflem 33839 pstmfval 33895 pstmxmet 33896 esumex 34030 msrval 35543 dfrdg2 35796 fvbigcup 35903 ctbssinf 37407 ptrest 37626 heiborlem1 37818 heiborlem3 37820 heibor 37828 dicval 41178 prjcrvfval 42641 aomclem1 43066 dfac21 43078 ntrrn 44135 ntrf 44136 dssmapntrcls 44141 fourierdlem70 46191 caragendifcl 46529 cnfsmf 46755 tposideq 48788 setrec1lem3 49208 setrec2fun 49211 |
| Copyright terms: Public domain | W3C validator |