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 3510 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3510 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | unexb 7460 | . . 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 3492 ∪ cun 3931 |
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 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 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 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-sn 4558 df-pr 4560 df-uni 4831 |
This theorem is referenced by: xpexg 7462 difex2 7471 difsnexi 7472 eldifpw 7479 pwuncl 7481 ordunpr 7530 soex 7615 fnse 7816 suppun 7839 tposexg 7895 wfrlem15 7958 tfrlem12 8014 tfrlem16 8018 elmapresaun 8433 ralxpmap 8448 undifixp 8486 undom 8593 domunsncan 8605 domssex2 8665 domssex 8666 mapunen 8674 fsuppunbi 8842 elfiun 8882 brwdom2 9025 unwdomg 9036 djuex 9325 djuexALT 9339 alephprc 9513 djudoml 9598 infunabs 9617 fin23lem11 9727 axdc2lem 9858 ttukeylem1 9919 fpwwe2lem13 10052 wunex2 10148 wuncval2 10157 hashunx 13735 hashf1lem1 13801 trclexlem 14342 trclun 14362 relexp0g 14369 relexpsucnnr 14372 isstruct2 16481 setsvalg 16500 setsid 16526 yonffth 17522 pwmndgplus 18038 dmdprdsplit2 19097 basdif0 21489 fiuncmp 21940 refun0 22051 ptbasfi 22117 dfac14lem 22153 ptrescn 22175 xkoptsub 22190 filconn 22419 isufil2 22444 ufileu 22455 filufint 22456 fmfnfmlem4 22493 fmfnfm 22494 fclsfnflim 22563 flimfnfcls 22564 ptcmplem1 22588 elply2 24713 plyss 24716 wlkp1lem4 27385 resf1o 30392 tocycfv 30678 tocycf 30686 locfinref 31004 esumsplit 31211 esumpad2 31214 sseqval 31545 bnj1149 31963 satfvsuc 32505 satf0suclem 32519 sat1el2xp 32523 fmlasuc0 32528 frrlem13 33032 ssltun1 33166 ssltun2 33167 altxpexg 33336 hfun 33536 refssfne 33603 topjoin 33610 bj-2uplex 34231 ptrest 34772 poimirlem3 34776 paddval 36814 elrfi 39169 rclexi 39853 rtrclexlem 39854 trclubgNEW 39856 clcnvlem 39861 cnvrcl0 39863 dfrtrcl5 39867 iunrelexp0 39925 relexpmulg 39933 relexp01min 39936 relexpxpmin 39940 brtrclfv2 39950 sge0resplit 42565 sge0split 42568 setsv 43415 setrec1lem4 44721 |
Copyright terms: Public domain | W3C validator |