Theorem elrp 9605

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 3991	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 9604	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 2889	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ∧ wa 103   ↔ wb 104   ∈ wcel 2141   class class class wbr 3987  ℝcr 7766  0cc0 7767   < clt 7947  ℝ⁺crp 9603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988  df-rp 9604

This theorem is referenced by:  elrpii  9606  nnrp  9613  rpgt0  9615  rpregt0  9617  ralrp  9625  rexrp  9626  rpaddcl  9627  rpmulcl  9628  rpdivcl  9629  rpgecl  9632  rphalflt  9633  ge0p1rp  9635  rpnegap  9636  negelrp  9637  ltsubrp  9640  ltaddrp  9641  difrp  9642  elrpd  9643  iccdil  9948  icccntr  9950  dfrp2  10213  expgt0  10502  sqrtdiv  10999  mulcn2  11268  ef01bndlem  11712  nconstwlpolem  14061