Theorem pnfex 10093

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 10092	. 2 ⊢ +∞ ∈ ℝ*
2	1	elexi 3213	1 ⊢ +∞ ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200  +∞cpnf 10071  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843  ax-un 6949  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-pnf 10076  df-xr 10078

This theorem is referenced by:  mnfxr  10096  elxnn0  11365  elxr  11950  xnegex  12039  xaddval  12054  xmulval  12056  xrinfmss  12140  hashgval  13120  hashinf  13122  hashfxnn0  13124  hashfOLD  13126  pcval  15549  pc0  15559  ramcl2  15720  iccpnfhmeo  22744  taylfval  24113  xrlimcnp  24695  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  sge0f1o  40599  sge0sup  40608  sge0pnfmpt  40662