![]() |
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 3482 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3482 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | unexb 7748 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | |
4 | 3 | biimpi 215 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
5 | 1, 2, 4 | syl2an 594 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 Vcvv 3462 ∪ cun 3944 |
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 2697 ax-sep 5296 ax-nul 5303 ax-pr 5425 ax-un 7738 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4323 df-sn 4624 df-pr 4626 df-uni 4906 |
This theorem is referenced by: xpexg 7750 unexd 7754 difex2 7760 difsnexi 7761 eldifpw 7768 pwuncl 7770 ordunpr 7827 soex 7926 fnse 8139 suppun 8190 tposexg 8247 frrlem13 8305 wfrlem15OLD 8345 tfrlem12 8411 tfrlem16 8415 elmapresaun 8901 ralxpmap 8917 undifixp 8955 undom 9089 undomOLD 9090 domunsncan 9102 domssex2 9167 domssex 9168 mapunen 9176 sbthfilem 9228 fsuppunbi 9425 elfiun 9466 brwdom2 9609 unwdomg 9620 djuex 9944 djuexALT 9958 alephprc 10135 djudoml 10220 infunabs 10241 fin23lem11 10351 axdc2lem 10482 ttukeylem1 10543 fpwwe2lem12 10676 wunex2 10772 wuncval2 10781 hashunx 14398 hashf1lem1 14468 hashf1lem1OLD 14469 trclexlem 14994 trclun 15014 relexp0g 15022 relexpsucnnr 15025 isstruct2 17146 setsvalg 17163 setsid 17205 yonffth 18304 pwmndgplus 18920 dmdprdsplit2 20042 basdif0 22944 fiuncmp 23396 refun0 23507 ptbasfi 23573 dfac14lem 23609 ptrescn 23631 xkoptsub 23646 filconn 23875 isufil2 23900 ufileu 23911 filufint 23912 fmfnfmlem4 23949 fmfnfm 23950 fclsfnflim 24019 flimfnfcls 24020 ptcmplem1 24044 elply2 26220 plyss 26223 noeta2 27811 etasslt2 27841 scutbdaybnd2lim 27844 wlkp1lem4 29610 resf1o 32644 tocycfv 32991 tocycf 32999 locfinref 33669 esumsplit 33899 esumpad2 33902 sseqval 34235 bnj1149 34650 satfvsuc 35202 satf0suclem 35216 sat1el2xp 35220 fmlasuc0 35225 altxpexg 35815 hfun 36015 refssfne 36083 topjoin 36090 bj-2uplex 36742 ptrest 37333 poimirlem3 37337 paddval 39510 evlselvlem 42276 elrfi 42388 rtrclexlem 43320 clcnvlem 43327 cnvrcl0 43329 dfrtrcl5 43333 iunrelexp0 43406 relexpxpmin 43421 brtrclfv2 43431 sge0resplit 46063 sge0split 46066 setsv 46986 setrec1lem4 48472 |
Copyright terms: Public domain | W3C validator |