Description: The union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16. (Contributed by NM, 1-Jul-1994)
Ref | Expression | ||
---|---|---|---|
Hypotheses | unex.1 | ⊢ 𝐴 ∈ V | |
unex.2 | ⊢ 𝐵 ∈ V | ||
Assertion | unex | ⊢ ( 𝐴 ∪ 𝐵 ) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unex.1 | ⊢ 𝐴 ∈ V | |
2 | unex.2 | ⊢ 𝐵 ∈ V | |
3 | unexg | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V ) | |
4 | 1 2 3 | mp2an | ⊢ ( 𝐴 ∪ 𝐵 ) ∈ V |