Theorem modfsummodslem1

Description: Lemma 1 for modfsummods . (Contributed by Alexander van der Vekens, 1-Sep-2018)

	Ref	Expression
Assertion	modfsummodslem1	|- ( A. k e. ( A u. { z } ) B e. ZZ -> [_ z / k ]_ B e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		vsnid	|- z e. { z }
2		elun2	|- ( z e. { z } -> z e. ( A u. { z } ) )
3	1 2	ax-mp	|- z e. ( A u. { z } )
4		rspcsbela	|- ( ( z e. ( A u. { z } ) /\ A. k e. ( A u. { z } ) B e. ZZ ) -> [_ z / k ]_ B e. ZZ )
5	3 4	mpan	|- ( A. k e. ( A u. { z } ) B e. ZZ -> [_ z / k ]_ B e. ZZ )