Metamath Proof Explorer


Theorem unex

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

Proof

Step Hyp Ref Expression
1 unex.1 𝐴 ∈ V
2 unex.2 𝐵 ∈ V
3 unexg ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴𝐵 ) ∈ V )
4 1 2 3 mp2an ( 𝐴𝐵 ) ∈ V