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

Theorem elxr 11354
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
elxr

Proof of Theorem elxr
StepHypRef Expression
1 df-xr 9653 . . 3
21eleq2i 2535 . 2
3 elun 3644 . 2
4 pnfex 11351 . . . . 5
5 mnfxr 11352 . . . . . 6
65elexi 3119 . . . . 5
74, 6elpr2 4048 . . . 4
87orbi2i 519 . . 3
9 3orass 976 . . 3
108, 9bitr4i 252 . 2
112, 3, 103bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  \/w3o 972  =wceq 1395  e.wcel 1818  u.cun 3473  {cpr 4031   cr 9512   cpnf 9646   cmnf 9647   cxr 9648
This theorem is referenced by:  xrnemnf  11357  xrnepnf  11358  xrltnr  11359  xrltnsym  11372  xrlttri  11374  xrlttr  11375  xrrebnd  11398  qbtwnxr  11428  xnegcl  11441  xnegneg  11442  xltnegi  11444  xaddf  11452  xnegid  11464  xaddcom  11466  xaddid1  11467  xnegdi  11469  xleadd1a  11474  xlt2add  11481  xsubge0  11482  xmullem  11485  xmulid1  11500  xmulgt0  11504  xmulasslem3  11507  xlemul1a  11509  xadddilem  11515  xadddi2  11518  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  isxmet2d  20830  blssioo  21300  ioombl1  21972  ismbf2d  22048  itg2seq  22149  xaddeq0  27573
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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-pow 4630  ax-un 6592  ax-cnex 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  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-rex 2813  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-pw 4014  df-sn 4030  df-pr 4032  df-uni 4250  df-pnf 9651  df-mnf 9652  df-xr 9653
  Copyright terms: Public domain W3C validator