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	⊢ 𝐴 ∈ V
	iunsuc.2	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	iunsuc	⊢ ∪ 𝑥 ∈ suc 𝐴 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iunsuc.1	⊢ 𝐴 ∈ V
2		iunsuc.2	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
3		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
4		iuneq1	⊢ ( suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) → ∪ 𝑥 ∈ suc 𝐴 𝐵 = ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝐴 } ) 𝐵 )
5	3 4	ax-mp	⊢ ∪ 𝑥 ∈ suc 𝐴 𝐵 = ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝐴 } ) 𝐵
6		iunxun	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝐴 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝐴 } 𝐵 )
7	1 2	iunxsn	⊢ ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶
8	7	uneq2i	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝐴 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 )
9	5 6 8	3eqtri	⊢ ∪ 𝑥 ∈ suc 𝐴 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 )