| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > unexg | Structured version Visualization version GIF version | ||
| Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) Prove unexg 7763 first and then unex 7764 and unexb 7767 from it. (Revised by BJ, 21-Jul-2025.) |
| Ref | Expression |
|---|---|
| unexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uniprg 4923 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)) | |
| 2 | prex 5437 | . . . 4 ⊢ {𝐴, 𝐵} ∈ V | |
| 3 | 2 | a1i 11 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) |
| 4 | 3 | uniexd 7762 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} ∈ V) |
| 5 | 1, 4 | eqeltrrd 2842 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Vcvv 3480 ∪ cun 3949 {cpr 4628 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-sn 4627 df-pr 4629 df-uni 4908 |
| This theorem is referenced by: unex 7764 unexb 7767 xpexg 7770 unexd 7774 difex2 7780 difsnexi 7781 eldifpw 7788 pwuncl 7790 ordunpr 7846 soex 7943 fnse 8158 suppun 8209 tposexg 8265 frrlem13 8323 wfrlem15OLD 8363 tfrlem12 8429 tfrlem16 8433 elmapresaun 8920 ralxpmap 8936 undifixp 8974 undom 9099 undomOLD 9100 domunsncan 9112 domssex2 9177 domssex 9178 mapunen 9186 sbthfilem 9238 fsuppunbi 9429 elfiun 9470 brwdom2 9613 unwdomg 9624 djuex 9948 djuexALT 9962 alephprc 10139 djudoml 10225 infunabs 10246 fin23lem11 10357 axdc2lem 10488 ttukeylem1 10549 fpwwe2lem12 10682 wunex2 10778 wuncval2 10787 hashunx 14425 hashf1lem1 14494 trclexlem 15033 trclun 15053 relexp0g 15061 relexpsucnnr 15064 isstruct2 17186 setsvalg 17203 setsid 17244 yonffth 18329 pwmndgplus 18948 dmdprdsplit2 20066 basdif0 22960 fiuncmp 23412 refun0 23523 ptbasfi 23589 dfac14lem 23625 ptrescn 23647 xkoptsub 23662 filconn 23891 isufil2 23916 ufileu 23927 filufint 23928 fmfnfmlem4 23965 fmfnfm 23966 fclsfnflim 24035 flimfnfcls 24036 ptcmplem1 24060 elply2 26235 plyss 26238 noeta2 27829 etasslt2 27859 scutbdaybnd2lim 27862 wlkp1lem4 29694 resf1o 32741 tocycfv 33129 tocycf 33137 locfinref 33840 esumsplit 34054 esumpad2 34057 sseqval 34390 bnj1149 34806 satfvsuc 35366 satf0suclem 35380 sat1el2xp 35384 fmlasuc0 35389 altxpexg 35979 hfun 36179 refssfne 36359 topjoin 36366 weiunse 36469 bj-2uplex 37023 ptrest 37626 poimirlem3 37630 paddval 39800 evlselvlem 42596 elrfi 42705 rtrclexlem 43629 clcnvlem 43636 cnvrcl0 43638 dfrtrcl5 43642 iunrelexp0 43715 relexpxpmin 43730 brtrclfv2 43740 sge0resplit 46421 sge0split 46424 setsv 47365 setrec1lem4 49209 |
| Copyright terms: Public domain | W3C validator |