Theorem eldiophelnn0

Description: Remove antecedent on B from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	eldiophelnn0	$$⊢A\in \mathrm{Dioph}\left(B\right)\to B\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eldiophb	$$⊢A\in \mathrm{Dioph}\left(B\right)\leftrightarrow \left(B\in {\mathbb{N}}_0\wedge \exists b\in {\mathbb{Z}}_{\ge B}\exists a\in \mathrm{mzPoly}\left(\left(1\dots b\right)\right)A=\left\{c|\exists d\in \left({{\mathbb{N}}_0}^{\left(1\dots b\right)}\right)\left(c={d\upharpoonright }_{\left(1\dots B\right)}\wedge a\left(d\right)=0\right)\right\}\right)$$
2	1	simplbi	$$⊢A\in \mathrm{Dioph}\left(B\right)\to B\in {\mathbb{N}}_0$$