Theorem eldiophelnn0

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

	Ref	Expression
Assertion	eldiophelnn0	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) → 𝐵 ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		eldiophb	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) ↔ ( 𝐵 ∈ ℕ0 ∧ ∃ 𝑏 ∈ ( ℤ≥ ‘ 𝐵 ) ∃ 𝑎 ∈ ( mzPoly ‘ ( 1 ... 𝑏 ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑏 ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ) )
2	1	simplbi	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) → 𝐵 ∈ ℕ0 )