![]() |
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 3484), 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 7745 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∪ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3471 ∪ cuni 4908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 ax-un 7740 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 df-ss 3964 df-uni 4909 |
This theorem is referenced by: unex 7748 iunpw 7773 elxp4 7930 elxp5 7931 1stval 7995 2ndval 7996 fo1st 8013 fo2nd 8014 cnvf1o 8116 brtpos2 8238 naddcllem 8697 ixpsnf1o 8957 dffi3 9455 cnfcom2 9726 cnfcom3lem 9727 cnfcom3 9728 ttrclse 9751 trcl 9752 rankc2 9895 rankxpl 9899 rankxpsuc 9906 acnlem 10072 dfac2a 10153 fin23lem14 10357 fin23lem16 10359 fin23lem17 10362 fin23lem38 10373 fin23lem39 10374 itunisuc 10443 axdc3lem2 10475 axcclem 10481 ac5b 10502 ttukey 10542 wunex2 10762 wuncval2 10771 intgru 10838 pnfex 11298 prdsvallem 17436 prdsval 17437 prdsds 17446 wunfunc 17887 wunfuncOLD 17888 wunnat 17946 wunnatOLD 17947 arwval 18032 catcfuccl 18108 catcfucclOLD 18109 catcxpccl 18198 catcxpcclOLD 18199 zrhval 21433 mreclatdemoBAD 23013 ptbasin2 23495 ptbasfi 23498 dfac14 23535 ptcmplem2 23970 ptcmplem3 23971 ptcmp 23975 cnextfvval 23982 cnextcn 23984 minveclem4a 25371 oldf 27797 precsexlem10 28127 xrge0tsmsbi 32785 dimval 33298 dimvalfi 33299 locfinreflem 33441 pstmfval 33497 pstmxmet 33498 esumex 33648 msrval 35148 dfrdg2 35391 fvbigcup 35498 ctbssinf 36885 ptrest 37092 heiborlem1 37284 heiborlem3 37286 heibor 37294 dicval 40649 prjcrvfval 42055 aomclem1 42478 dfac21 42490 ntrrn 43552 ntrf 43553 dssmapntrcls 43558 fourierdlem70 45564 caragendifcl 45902 cnfsmf 46128 setrec1lem3 48120 setrec2fun 48123 |
Copyright terms: Public domain | W3C validator |