Theorem nqex 7295

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

Assertion

Ref	Expression
nqex	|- Q. e. _V

Proof of Theorem nqex

Step	Hyp	Ref	Expression
1		df-nqqs 7280	. 2 |- Q. = ( ( N. X. N. ) /. ~Q )
2		niex 7244	. . . 4 |- N. e. _V
3	2, 2	xpex 4713	. . 3 |- ( N. X. N. ) e. _V
4	3	qsex 6549	. 2 |- ( ( N. X. N. ) /. ~Q ) e. _V
5	1, 4	eqeltri 2237	1 |- Q. e. _V

Syntax hints:   e. wcel 2135   _Vcvv 2721   X. cxp 4596   /.cqs 6491   N.cnpi 7204   ~Q ceq 7211   Q.cnq 7212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4091  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-iinf 4559

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2723  df-sbc 2947  df-csb 3041  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-int 3819  df-iun 3862  df-br 3977  df-opab 4038  df-mpt 4039  df-id 4265  df-iom 4562  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-f1 5187  df-fo 5188  df-f1o 5189  df-fv 5190  df-qs 6498  df-ni 7236  df-nqqs 7280

This theorem is referenced by:  npex  7405  elinp  7406  genipv  7441  genpelxp  7443  genpelvl  7444  genpelvu  7445  genipdm  7448  ltnqex  7481  gtnqex  7482  ltexprlemell  7530  ltexprlemelu  7531  ltexprlempr  7540  recexprlemell  7554  recexprlemelu  7555  recexprlempr  7564  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemcl  7585  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlemladd  7590  cauappcvgprlem1  7591  cauappcvgprlem2  7592  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlem2  7612  caucvgprprlemell  7617  caucvgprprlemelu  7618  caucvgprprlemml  7626  caucvgprprlemmu  7627  caucvgprprlemcl  7636  caucvgprprlemexbt  7638  caucvgprprlem2  7642  suplocexprlem2b  7646  suplocexprlemlub  7656