Theorem nqex

Description: The class of positive fractions exists. (Contributed by NM, 16-Aug-1995) (Revised by Mario Carneiro, 27-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nqex	$$⊢𝑸\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-nq	$$⊢𝑸=\left\{y\in \left(𝑵\times 𝑵\right)|\forall x\in \left(𝑵\times 𝑵\right)\left(y{~}_{𝑸}x\to \neg 2^{nd}\left(x\right){<}_{𝑵}{2}^{nd}\left(y\right)\right)\right\}$$
2		niex	$$⊢𝑵\in \mathrm{V}$$
3	2 2	xpex	$$⊢𝑵\times 𝑵\in \mathrm{V}$$
4	1 3	rabex2	$$⊢𝑸\in \mathrm{V}$$