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	|- ( A e. V -> U. suc A = ( U. A u. A ) )

Proof

Step	Hyp	Ref	Expression
1		df-suc	|- suc A = ( A u. { A } )
2	1	unieqi	|- U. suc A = U. ( A u. { A } )
3	2	a1i	|- ( A e. V -> U. suc A = U. ( A u. { A } ) )
4		uniun	|- U. ( A u. { A } ) = ( U. A u. U. { A } )
5	4	a1i	|- ( A e. V -> U. ( A u. { A } ) = ( U. A u. U. { A } ) )
6		unisng	|- ( A e. V -> U. { A } = A )
7	6	uneq2d	|- ( A e. V -> ( U. A u. U. { A } ) = ( U. A u. A ) )
8	3 5 7	3eqtrd	|- ( A e. V -> U. suc A = ( U. A u. A ) )