Theorem unisucs

Description: The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993) Extract from unisuc . (Revised by BJ, 28-Dec-2024)

	Ref	Expression
Assertion	unisucs	⊢ ( 𝐴 ∈ 𝑉 → ∪ suc 𝐴 = ( ∪ 𝐴 ∪ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2	1	unieqi	⊢ ∪ suc 𝐴 = ∪ ( 𝐴 ∪ { 𝐴 } )
3	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∪ suc 𝐴 = ∪ ( 𝐴 ∪ { 𝐴 } ) )
4		uniun	⊢ ∪ ( 𝐴 ∪ { 𝐴 } ) = ( ∪ 𝐴 ∪ ∪ { 𝐴 } )
5	4	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∪ ( 𝐴 ∪ { 𝐴 } ) = ( ∪ 𝐴 ∪ ∪ { 𝐴 } ) )
6		unisng	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )
7	6	uneq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝐴 ∪ ∪ { 𝐴 } ) = ( ∪ 𝐴 ∪ 𝐴 ) )
8	3 5 7	3eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ∪ suc 𝐴 = ( ∪ 𝐴 ∪ 𝐴 ) )