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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 uniprg ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) )
2 prex { 𝐴 , 𝐵 } ∈ V
3 2 a1i ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 , 𝐵 } ∈ V )
4 3 uniexd ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 , 𝐵 } ∈ V )
5 1 4 eqeltrrd ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝐵 ) ∈ V )