Theorem bcxmaslem1

Description: Lemma for bcxmas . (Contributed by Paul Chapman, 18-May-2007)

	Ref	Expression
Assertion	bcxmaslem1	|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( A = B -> ( N + A ) = ( N + B ) )
2		id	|- ( A = B -> A = B )
3	1 2	oveq12d	|- ( A = B -> ( ( N + A ) _C A ) = ( ( N + B ) _C B ) )