| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > unex | 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, 1-Jul-1994.) |
| Ref | Expression |
|---|---|
| unex.1 | ⊢ 𝐴 ∈ V |
| unex.2 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| unex | ⊢ (𝐴 ∪ 𝐵) ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unex.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | unex.2 | . 2 ⊢ 𝐵 ∈ V | |
| 3 | unexg 7763 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∪ 𝐵) ∈ V |
| Copyright terms: Public domain | W3C validator |