Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unexg | Structured version Visualization version GIF version |
Description: A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
Ref | Expression |
---|---|
unexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3513 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3513 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | unexb 7459 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | |
4 | 3 | biimpi 217 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
5 | 1, 2, 4 | syl2an 595 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 Vcvv 3495 ∪ cun 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-sn 4560 df-pr 4562 df-uni 4833 |
This theorem is referenced by: xpexg 7461 difex2 7470 difsnexi 7471 eldifpw 7478 pwuncl 7480 ordunpr 7529 soex 7614 fnse 7818 suppun 7841 tposexg 7897 wfrlem15 7960 tfrlem12 8016 tfrlem16 8020 elmapresaun 8434 ralxpmap 8449 undifixp 8487 undom 8594 domunsncan 8606 domssex2 8666 domssex 8667 mapunen 8675 fsuppunbi 8843 elfiun 8883 brwdom2 9026 unwdomg 9037 djuex 9326 djuexALT 9340 alephprc 9514 djudoml 9599 infunabs 9618 fin23lem11 9728 axdc2lem 9859 ttukeylem1 9920 fpwwe2lem13 10053 wunex2 10149 wuncval2 10158 hashunx 13737 hashf1lem1 13803 trclexlem 14344 trclun 14364 relexp0g 14371 relexpsucnnr 14374 isstruct2 16483 setsvalg 16502 setsid 16528 yonffth 17524 pwmndgplus 18040 dmdprdsplit2 19099 basdif0 21491 fiuncmp 21942 refun0 22053 ptbasfi 22119 dfac14lem 22155 ptrescn 22177 xkoptsub 22192 filconn 22421 isufil2 22446 ufileu 22457 filufint 22458 fmfnfmlem4 22495 fmfnfm 22496 fclsfnflim 22565 flimfnfcls 22566 ptcmplem1 22590 elply2 24715 plyss 24718 wlkp1lem4 27386 resf1o 30393 tocycfv 30679 tocycf 30687 locfinref 31005 esumsplit 31212 esumpad2 31215 sseqval 31546 bnj1149 31964 satfvsuc 32506 satf0suclem 32520 sat1el2xp 32524 fmlasuc0 32529 frrlem13 33033 ssltun1 33167 ssltun2 33168 altxpexg 33337 hfun 33537 refssfne 33604 topjoin 33611 bj-2uplex 34232 ptrest 34773 poimirlem3 34777 paddval 36816 elrfi 39171 rclexi 39855 rtrclexlem 39856 trclubgNEW 39858 clcnvlem 39863 cnvrcl0 39865 dfrtrcl5 39869 iunrelexp0 39927 relexpmulg 39935 relexp01min 39938 relexpxpmin 39942 brtrclfv2 39952 sge0resplit 42569 sge0split 42572 setsv 43419 setrec1lem4 44691 |
Copyright terms: Public domain | W3C validator |