Theorem nqercl

Description: Corollary of nqereu : closure of /Q . (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nqercl	$$⊢A\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(A\right)\in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		nqerf	$$⊢{/}_{𝑸}:𝑵\times 𝑵⟶𝑸$$
2	1	ffvelcdmi	$$⊢A\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(A\right)\in 𝑸$$