This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (𝑵 \times 𝑵) \to /_{𝑸} (A) \in 𝑸$

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