Theorem unipr

Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 23-Aug-1993) (Proof shortened by BJ, 1-Sep-2024)

	Ref	Expression
Hypotheses	unipr.1	⊢ 𝐴 ∈ V
	unipr.2	⊢ 𝐵 ∈ V
Assertion	unipr	⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		unipr.1	⊢ 𝐴 ∈ V
2		unipr.2	⊢ 𝐵 ∈ V
3		uniprg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
4	1 2 3	mp2an	⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )