![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unexd | Structured version Visualization version GIF version |
Description: The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
Ref | Expression |
---|---|
unexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
unexd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
Ref | Expression |
---|---|
unexd | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | unexd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
3 | unexg 7762 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3478 ∪ cun 3961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-sn 4632 df-pr 4634 df-uni 4913 |
This theorem is referenced by: sexp2 8170 sexp3 8177 ssltun1 27868 ssltun2 27869 addsproplem2 28018 addsuniflem 28049 ssltmul1 28188 ssltmul2 28189 precsexlem11 28256 suppun2 32699 elrspunsn 33437 ofun 42256 tfsconcatun 43327 rclexi 43605 rtrclexlem 43606 trclubgNEW 43608 cnvrcl0 43615 dfrtrcl5 43619 iunrelexp0 43692 relexpmulg 43700 relexp01min 43703 clnbgrval 47747 |
Copyright terms: Public domain | W3C validator |