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

Proof

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