Metamath Proof Explorer

Theorem unexg

Description: The union of two sets is a set. Corollary 5.8 of TakeutiZaring p. 16. (Contributed by NM, 18-Sep-2006) Prove unexg first and then unex and unexb from it. (Revised by BJ, 21-Jul-2025)

Ref Expression
Assertion unexg ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V

Proof

Step Hyp Ref Expression
1 uniprg ⊢ A ∈ V ∧ B ∈ W → ⋃ A B = A ∪ B
2 prex ⊢ A B ∈ V
3 2 a1i ⊢ A ∈ V ∧ B ∈ W → A B ∈ V
4 3 uniexd ⊢ A ∈ V ∧ B ∈ W → ⋃ A B ∈ V
5 1 4 eqeltrrd ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V