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

Metamath Proof Explorer

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 V$

Proof

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