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 e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )

Proof

Step Hyp Ref Expression
1 nqerf 
 |-  /Q : ( N. X. N. ) --> Q.
2 1 ffvelrni 
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )