Theorem pnfex 10375

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

Syntax hints:   ∈ wcel 2158  Vcvv 3390  +∞cpnf 10353  ℝ^*cxr 10355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-pow 5032  ax-un 7176  ax-cnex 10274

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rex 3101  df-v 3392  df-un 3771  df-in 3773  df-ss 3780  df-pw 4350  df-sn 4368  df-pr 4370  df-uni 4627  df-pnf 10358  df-xr 10360

This theorem is referenced by:  mnfxr  10378  elxnn0  11627  elxr  12162  xnegex  12253  xaddval  12268  xmulval  12270  xrinfmss  12354  hashgval  13336  hashinf  13338  hashfxnn0  13340  hashfOLD  13342  pcval  15762  pc0  15772  ramcl2  15933  iccpnfhmeo  22953  taylfval  24323  xrlimcnp  24905  xrge0iifcv  30302  xrge0iifiso  30303  xrge0iifhom  30305  sge0f1o  41075  sge0sup  41084  sge0pnfmpt  41138