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 3451 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3451 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | unexb 7607 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | |
4 | 3 | biimpi 215 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
5 | 1, 2, 4 | syl2an 596 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2107 Vcvv 3433 ∪ cun 3886 |
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 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 ax-un 7597 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-sn 4563 df-pr 4565 df-uni 4841 |
This theorem is referenced by: xpexg 7609 unexd 7613 difex2 7619 difsnexi 7620 eldifpw 7627 pwuncl 7629 ordunpr 7682 soex 7777 fnse 7983 suppun 8009 tposexg 8065 frrlem13 8123 wfrlem15OLD 8163 tfrlem12 8229 tfrlem16 8233 elmapresaun 8677 ralxpmap 8693 undifixp 8731 undom 8855 undomOLD 8856 domunsncan 8868 domssex2 8933 domssex 8934 mapunen 8942 sbthfilem 8993 fsuppunbi 9158 elfiun 9198 brwdom2 9341 unwdomg 9352 djuex 9675 djuexALT 9689 alephprc 9864 djudoml 9949 infunabs 9972 fin23lem11 10082 axdc2lem 10213 ttukeylem1 10274 fpwwe2lem12 10407 wunex2 10503 wuncval2 10512 hashunx 14110 hashf1lem1 14177 hashf1lem1OLD 14178 trclexlem 14714 trclun 14734 relexp0g 14742 relexpsucnnr 14745 isstruct2 16859 setsvalg 16876 setsid 16918 yonffth 18011 pwmndgplus 18583 dmdprdsplit2 19658 basdif0 22112 fiuncmp 22564 refun0 22675 ptbasfi 22741 dfac14lem 22777 ptrescn 22799 xkoptsub 22814 filconn 23043 isufil2 23068 ufileu 23079 filufint 23080 fmfnfmlem4 23117 fmfnfm 23118 fclsfnflim 23187 flimfnfcls 23188 ptcmplem1 23212 elply2 25366 plyss 25369 wlkp1lem4 28053 resf1o 31074 tocycfv 31385 tocycf 31393 locfinref 31800 esumsplit 32030 esumpad2 32033 sseqval 32364 bnj1149 32781 satfvsuc 33332 satf0suclem 33346 sat1el2xp 33350 fmlasuc0 33355 noeta2 33988 etasslt2 34017 scutbdaybnd2lim 34020 altxpexg 34289 hfun 34489 refssfne 34556 topjoin 34563 bj-2uplex 35221 ptrest 35785 poimirlem3 35789 paddval 37819 elrfi 40523 rclexi 41230 rtrclexlem 41231 trclubgNEW 41233 clcnvlem 41238 cnvrcl0 41240 dfrtrcl5 41244 iunrelexp0 41317 relexpmulg 41325 relexp01min 41328 relexpxpmin 41332 brtrclfv2 41342 sge0resplit 43951 sge0split 43954 setsv 44841 setrec1lem4 46407 |
Copyright terms: Public domain | W3C validator |