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 3185 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3185 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | unexb 6856 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | |
4 | 3 | biimpi 205 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
5 | 1, 2, 4 | syl2an 493 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 |
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-in 3547 df-ss 3554 df-nul 3875 df-sn 4126 df-pr 4128 df-uni 4373 |
This theorem is referenced by: xpexg 6858 difex2 6863 difsnexi 6864 eldifpw 6868 ordunpr 6918 soex 7002 fnse 7181 suppun 7202 tposexg 7253 wfrlem15 7316 tfrlem12 7372 tfrlem16 7376 ralxpmap 7793 undifixp 7830 undom 7933 domunsncan 7945 domssex2 8005 domssex 8006 mapunen 8014 fsuppunbi 8179 elfiun 8219 brwdom2 8361 unwdomg 8372 alephprc 8805 cdadom3 8893 infunabs 8912 fin23lem11 9022 axdc2lem 9153 ttukeylem1 9214 fpwwe2lem13 9343 wunex2 9439 wuncval2 9448 hashunx 13036 hashf1lem1 13096 trclexlem 13581 trclun 13603 relexp0g 13610 relexpsucnnr 13613 isstruct2 15704 setsvalg 15719 setsid 15742 yonffth 16747 dmdprdsplit2 18268 basdif0 20568 fiuncmp 21017 refun0 21128 ptbasfi 21194 dfac14lem 21230 ptrescn 21252 xkoptsub 21267 filcon 21497 isufil2 21522 ufileu 21533 filufint 21534 fmfnfmlem4 21571 fmfnfm 21572 fclsfnflim 21641 flimfnfcls 21642 ptcmplem1 21666 elply2 23756 plyss 23759 uhgraun 25840 umgraun 25857 vdgrun 26428 resf1o 28893 locfinref 29236 esumsplit 29442 esumpad2 29445 sseqval 29777 bnj1149 30117 nofulllem4 31104 altxpexg 31255 hfun 31455 refssfne 31523 topjoin 31530 bj-2uplex 32203 ptrest 32578 poimirlem3 32582 paddval 34102 elrfi 36275 elmapresaun 36352 rclexi 36941 rtrclexlem 36942 trclubgNEW 36944 clcnvlem 36949 cnvrcl0 36951 dfrtrcl5 36955 iunrelexp0 37013 relexpmulg 37021 relexp01min 37024 relexpxpmin 37028 brtrclfv2 37038 sge0resplit 39299 sge0split 39302 1wlkp1lem4 40885 setrec1lem4 42236 |
Copyright terms: Public domain | W3C validator |