Theorem bcxmaslem1

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

	Ref	Expression
Assertion	bcxmaslem1	$$⊢A=B\to \left(\genfrac{}{}{0ex}{}{N+A}{A}\right)=\left(\genfrac{}{}{0ex}{}{N+B}{B}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢A=B\to N+A=N+B$$
2		id	$$⊢A=B\to A=B$$
3	1 2	oveq12d	$$⊢A=B\to \left(\genfrac{}{}{0ex}{}{N+A}{A}\right)=\left(\genfrac{}{}{0ex}{}{N+B}{B}\right)$$