Theorem elrp 9880

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
elrp	⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem elrp

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4090	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 9879	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 2963	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2200   class class class wbr 4086  ℝcr 8021  0cc0 8022   < clt 8204  ℝ⁺crp 9878

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-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-rp 9879

This theorem is referenced by:  elrpii  9881  nnrp  9888  rpgt0  9890  rpregt0  9892  ralrp  9900  rexrp  9901  rpaddcl  9902  rpmulcl  9903  rpdivcl  9904  rpgecl  9907  rphalflt  9908  ge0p1rp  9910  rpnegap  9911  negelrp  9912  ltsubrp  9915  ltaddrp  9916  difrp  9917  elrpd  9918  iccdil  10223  icccntr  10225  dfrp2  10513  expgt0  10824  sqrtdiv  11593  mulcn2  11863  ef01bndlem  12307  nconstwlpolem  16605