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

Theorem elnpi 9420
 Description: Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
elnpi
Distinct variable group:   ,,

Proof of Theorem elnpi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3089 . 2
2 simpl1 1008 . 2
3 psseq2 3553 . . . . . 6
4 psseq1 3552 . . . . . 6
53, 4anbi12d 715 . . . . 5
6 eleq2 2496 . . . . . . . . 9
76imbi2d 317 . . . . . . . 8
87albidv 1761 . . . . . . 7
9 rexeq 3023 . . . . . . 7
108, 9anbi12d 715 . . . . . 6
1110raleqbi1dv 3030 . . . . 5
125, 11anbi12d 715 . . . 4
13 df-np 9413 . . . 4
1412, 13elab2g 3219 . . 3
15 id 22 . . . . . 6
16153expib 1208 . . . . 5
17 3simpc 1004 . . . . 5
1816, 17impbid1 206 . . . 4
1918anbi1d 709 . . 3
2014, 19bitrd 256 . 2
211, 2, 20pm5.21nii 354 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982  wal 1435   wceq 1437   wcel 1872  wral 2771  wrex 2772  cvv 3080   wpss 3437  c0 3761   class class class wbr 4423  cnq 9284   cltq 9290  cnp 9291 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401 This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-v 3082  df-in 3443  df-ss 3450  df-pss 3452  df-np 9413 This theorem is referenced by:  prn0  9421  prpssnq  9422  prcdnq  9425  prnmax  9427
 Copyright terms: Public domain W3C validator