![]() |
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 3461), 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 7682 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3448 ∪ cuni 4870 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5261 ax-un 7677 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-uni 4871 |
This theorem is referenced by: unex 7685 iunpw 7710 elxp4 7864 elxp5 7865 1stval 7928 2ndval 7929 fo1st 7946 fo2nd 7947 cnvf1o 8048 brtpos2 8168 naddcllem 8627 ixpsnf1o 8883 dffi3 9374 cnfcom2 9645 cnfcom3lem 9646 cnfcom3 9647 ttrclse 9670 trcl 9671 rankc2 9814 rankxpl 9818 rankxpsuc 9825 acnlem 9991 dfac2a 10072 fin23lem14 10276 fin23lem16 10278 fin23lem17 10281 fin23lem38 10292 fin23lem39 10293 itunisuc 10362 axdc3lem2 10394 axcclem 10400 ac5b 10421 ttukey 10461 wunex2 10681 wuncval2 10690 intgru 10757 pnfex 11215 prdsvallem 17343 prdsval 17344 prdsds 17353 wunfunc 17792 wunfuncOLD 17793 wunnat 17850 wunnatOLD 17851 arwval 17936 catcfuccl 18012 catcfucclOLD 18013 catcxpccl 18102 catcxpcclOLD 18103 zrhval 20924 mreclatdemoBAD 22463 ptbasin2 22945 ptbasfi 22948 dfac14 22985 ptcmplem2 23420 ptcmplem3 23421 ptcmp 23425 cnextfvval 23432 cnextcn 23434 minveclem4a 24810 oldf 27209 xrge0tsmsbi 31942 dimval 32340 dimvalfi 32341 locfinreflem 32461 pstmfval 32517 pstmxmet 32518 esumex 32668 msrval 34172 dfrdg2 34409 fvbigcup 34516 ctbssinf 35906 ptrest 36106 heiborlem1 36299 heiborlem3 36301 heibor 36309 dicval 39668 prjcrvfval 40998 aomclem1 41410 dfac21 41422 ntrrn 42468 ntrf 42469 dssmapntrcls 42474 fourierdlem70 44491 caragendifcl 44829 cnfsmf 45055 setrec1lem3 47208 setrec2fun 47211 |
Copyright terms: Public domain | W3C validator |