Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unex | Structured version Visualization version GIF version |
Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
Ref | Expression |
---|---|
unex.1 | ⊢ 𝐴 ∈ V |
unex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
unex | ⊢ (𝐴 ∪ 𝐵) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unex.1 | . . 3 ⊢ 𝐴 ∈ V | |
2 | unex.2 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | unipr 4385 | . 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵) |
4 | prex 4836 | . . 3 ⊢ {𝐴, 𝐵} ∈ V | |
5 | 4 | uniex 6851 | . 2 ⊢ ∪ {𝐴, 𝐵} ∈ V |
6 | 3, 5 | eqeltrri 2685 | 1 ⊢ (𝐴 ∪ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 {cpr 4127 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-v 3175 df-dif 3543 df-un 3545 df-nul 3875 df-sn 4126 df-pr 4128 df-uni 4373 |
This theorem is referenced by: tpex 6855 unexb 6856 fvclex 7031 ralxpmap 7793 unen 7925 enfixsn 7954 sbthlem10 7964 unxpdomlem3 8051 isinf 8058 findcard2 8085 ac6sfi 8089 pwfilem 8143 fiin 8211 cnfcomlem 8479 trcl 8487 tc2 8501 rankxpu 8622 rankxplim 8625 rankxplim3 8627 r0weon 8718 infxpenlem 8719 dfac4 8828 dfac2 8836 kmlem2 8856 cdafn 8874 cfsmolem 8975 isfin1-3 9091 axdc2lem 9153 axdc3lem4 9158 axcclem 9162 ttukeylem3 9216 gchac 9382 wunex2 9439 wuncval2 9448 inar1 9476 nn0ex 11175 xrex 11705 hashbclem 13093 incexclem 14407 ramub1lem2 15569 prdsval 15938 imasval 15994 ipoval 16977 fpwipodrs 16987 plusffval 17070 staffval 18670 scaffval 18704 lpival 19066 psrval 19183 xrsex 19580 ipffval 19812 islindf4 19996 neitr 20794 leordtval2 20826 comppfsc 21145 1stckgen 21167 dfac14 21231 ptcmpfi 21426 hausflim 21595 flimclslem 21598 alexsubALTlem2 21662 nmfval 22203 icccmplem2 22434 tchex 22824 tchnmfval 22835 taylfval 23917 legval 25279 axlowdimlem15 25636 axlowdim 25641 eengv 25659 uhgrunop 25741 upgrunop 25785 umgrunop 25787 constr3lem1 26173 constr3cyclpe 26191 3v3e3cycl2 26192 padct 28885 ordtconlem1 29298 sxbrsigalem2 29675 bnj918 30090 subfacp1lem3 30418 subfacp1lem5 30420 erdszelem8 30434 mrexval 30652 mrsubcv 30661 mrsubff 30663 mrsubccat 30669 elmrsubrn 30671 finixpnum 32564 poimirlem4 32583 poimirlem15 32594 poimirlem28 32607 rrnval 32796 lsatset 33295 ldualset 33430 pclfinN 34204 dvaset 35311 dvhset 35388 hlhilset 36244 elrfi 36275 istopclsd 36281 mzpcompact2lem 36332 eldioph2lem1 36341 eldioph2lem2 36342 eldioph4b 36393 diophren 36395 ttac 36621 pwslnmlem2 36681 dfacbasgrp 36697 mendval 36772 idomsubgmo 36795 superuncl 36892 ssuncl 36894 sssymdifcl 36896 rclexi 36941 trclexi 36946 rtrclexi 36947 dfrtrcl5 36955 dfrcl2 36985 comptiunov2i 37017 cotrclrcl 37053 frege83 37260 frege110 37287 frege133 37310 clsk1indlem3 37361 isotone1 37366 fnchoice 38211 limcresiooub 38709 limcresioolb 38710 fourierdlem48 39047 fourierdlem49 39048 fourierdlem102 39101 fourierdlem114 39113 sge0resplit 39299 elpglem2 42254 |
Copyright terms: Public domain | W3C validator |