Theorem pnfex 10294

Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
pnfex	⊢ +∞ ∈ V

Proof of Theorem pnfex

Step	Hyp	Ref	Expression
1		pnfxr 10293	. 2 ⊢ +∞ ∈ ℝ*
2	1	elexi 3362	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 2144  Vcvv 3349  +∞cpnf 10272  ℝ^*cxr 10274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-pow 4971  ax-un 7095  ax-cnex 10193

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rex 3066  df-v 3351  df-un 3726  df-in 3728  df-ss 3735  df-pw 4297  df-sn 4315  df-pr 4317  df-uni 4573  df-pnf 10277  df-xr 10279

This theorem is referenced by:  mnfxr  10297  elxnn0  11566  elxr  12154  xnegex  12243  xaddval  12258  xmulval  12260  xrinfmss  12344  hashgval  13323  hashinf  13325  hashfxnn0  13327  hashfOLD  13329  pcval  15755  pc0  15765  ramcl2  15926  iccpnfhmeo  22963  taylfval  24332  xrlimcnp  24915  xrge0iifcv  30314  xrge0iifiso  30315  xrge0iifhom  30317  sge0f1o  41110  sge0sup  41119  sge0pnfmpt  41173