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

Theorem elpqn 9368
 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 9355 . . 3
2 ssrab2 3500 . . 3
31, 2eqsstri 3448 . 2
43sseli 3414 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wcel 1904  wral 2756  crab 2760   class class class wbr 4395   cxp 4837  cfv 5589  c2nd 6811  cnpi 9287   clti 9290   ceq 9294  cnq 9295 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-in 3397  df-ss 3404  df-nq 9355 This theorem is referenced by:  nqereu  9372  nqerid  9376  enqeq  9377  addpqnq  9381  mulpqnq  9384  ordpinq  9386  addclnq  9388  mulclnq  9390  addnqf  9391  mulnqf  9392  adderpq  9399  mulerpq  9400  addassnq  9401  mulassnq  9402  distrnq  9404  mulidnq  9406  recmulnq  9407  ltsonq  9412  lterpq  9413  ltanq  9414  ltmnq  9415  ltexnq  9418  archnq  9423  wuncn  9612
 Copyright terms: Public domain W3C validator