MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpqn Unicode version

Theorem elpqn 9324
Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
elpqn

Proof of Theorem elpqn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nq 9311 . . 3
2 ssrab2 3584 . . 3
31, 2eqsstri 3533 . 2
43sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  A.wral 2807  {crab 2811   class class class wbr 4452  X.cxp 5002  `cfv 5593   c2nd 6799   cnpi 9243   clti 9246   ceq 9250   cnq 9251
This theorem is referenced by:  nqereu  9328  nqerid  9332  enqeq  9333  addpqnq  9337  mulpqnq  9340  ordpinq  9342  addclnq  9344  mulclnq  9346  addnqf  9347  mulnqf  9348  adderpq  9355  mulerpq  9356  addassnq  9357  mulassnq  9358  distrnq  9360  mulidnq  9362  recmulnq  9363  ltsonq  9368  lterpq  9369  ltanq  9370  ltmnq  9371  ltexnq  9374  archnq  9379  wuncn  9568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3482  df-ss 3489  df-nq 9311
  Copyright terms: Public domain W3C validator