Theorem nqex 7364

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 7349	. 2 |- Q. = ( ( N. X. N. ) /. ~Q )
2		niex 7313	. . . 4 |- N. e. _V
3	2, 2	xpex 4743	. . 3 |- ( N. X. N. ) e. _V
4	3	qsex 6594	. 2 |- ( ( N. X. N. ) /. ~Q ) e. _V
5	1, 4	eqeltri 2250	1 |- Q. e. _V

Syntax hints:   e. wcel 2148   _Vcvv 2739   X. cxp 4626   /.cqs 6536   N.cnpi 7273   ~Q ceq 7280   Q.cnq 7281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-iinf 4589

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-qs 6543  df-ni 7305  df-nqqs 7349

This theorem is referenced by:  npex  7474  elinp  7475  genipv  7510  genpelxp  7512  genpelvl  7513  genpelvu  7514  genipdm  7517  ltnqex  7550  gtnqex  7551  ltexprlemell  7599  ltexprlemelu  7600  ltexprlempr  7609  recexprlemell  7623  recexprlemelu  7624  recexprlempr  7633  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemcl  7654  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlemladd  7659  cauappcvgprlem1  7660  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemcl  7705  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocexprlem2b  7715  suplocexprlemlub  7725