Theorem iunsuc

Description: Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	iunsuc.1	|- A e. _V
	iunsuc.2	|- ( x = A -> B = C )
Assertion	iunsuc	|- U_ x e. suc A B = ( U_ x e. A B u. C )

Proof

Step	Hyp	Ref	Expression
1		iunsuc.1	|- A e. _V
2		iunsuc.2	|- ( x = A -> B = C )
3		df-suc	|- suc A = ( A u. { A } )
4		iuneq1	|- ( suc A = ( A u. { A } ) -> U_ x e. suc A B = U_ x e. ( A u. { A } ) B )
5	3 4	ax-mp	|- U_ x e. suc A B = U_ x e. ( A u. { A } ) B
6		iunxun	|- U_ x e. ( A u. { A } ) B = ( U_ x e. A B u. U_ x e. { A } B )
7	1 2	iunxsn	|- U_ x e. { A } B = C
8	7	uneq2i	|- ( U_ x e. A B u. U_ x e. { A } B ) = ( U_ x e. A B u. C )
9	5 6 8	3eqtri	|- U_ x e. suc A B = ( U_ x e. A B u. C )