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

Theorem pnfex 11351
Description: Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
pnfex

Proof of Theorem pnfex
StepHypRef Expression
1 pnfxr 11350 . 2
21elexi 3119 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109   cpnf 9646   cxr 9648
This theorem is referenced by:  mnfxr  11352  elxr  11354  xnegex  11436  xaddval  11451  xmulval  11453  xrinfmss  11530  xrinfm0  11557  hashgval  12408  hashinf  12410  hashf  12412  pcval  14368  pc0  14378  ramcl2  14534  iccpnfhmeo  21445  taylfval  22754  xrlimcnp  23298  vdgrf  24898  xrge0iifcv  27916  xrge0iifiso  27917  xrge0iifhom  27919
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-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-xr 9653
  Copyright terms: Public domain W3C validator