Theorem pnfex 9972

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

Assertion

Ref	Expression
pnfex	⊢ +∞ ∈ V

Proof of Theorem pnfex

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  +∞cpnf 9950  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769  ax-un 6847  ax-cnex 9871

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4373  df-pnf 9955  df-xr 9957

This theorem is referenced by:  mnfxr  9975  elxnn0  11242  elxr  11826  xnegex  11913  xaddval  11928  xmulval  11930  xrinfmss  12012  hashgval  12982  hashinf  12984  hashfxnn0  12986  hashfOLD  12988  pcval  15387  pc0  15397  ramcl2  15558  iccpnfhmeo  22552  taylfval  23917  xrlimcnp  24495  vdgrf  26425  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  sge0f1o  39275  sge0sup  39284  sge0pnfmpt  39338