Theorem nqercl

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

	Ref	Expression
Assertion	nqercl	⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )

Proof

Step	Hyp	Ref	Expression
1		nqerf	⊢ [Q] : ( N × N ) ⟶ Q
2	1	ffvelrni	⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )