Metamath Proof Explorer
Description: The union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16.
(Contributed by NM, 1Jul1994)


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 
1 2

unipr 
⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) 
4 

prex 
⊢ { 𝐴 , 𝐵 } ∈ V 
5 
4

uniex 
⊢ ∪ { 𝐴 , 𝐵 } ∈ V 
6 
3 5

eqeltrri 
⊢ ( 𝐴 ∪ 𝐵 ) ∈ V 