Theorem elv 2804

Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2803), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)

Hypothesis

Ref	Expression
elv.1	⊢ (𝑥 ∈ V → 𝜑)

Assertion

Ref	Expression
elv	⊢ 𝜑

Proof of Theorem elv

Step	Hyp	Ref	Expression
1		vex 2803	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2200  Vcvv 2800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  xpiindim  4865  disjxp1  6396  ixpiinm  6888  ixpsnf1o  6900  modom  6989  eqsndc  7088  iunfidisj  7136  ssfii  7164  fifo  7170  dcfi  7171  omp1eomlem  7284  exmidomniim  7331  bcval5  11015  rexfiuz  11540  fsum2dlemstep  11985  fsumcnv  11988  fisumcom2  11989  fsumconst  12005  modfsummodlemstep  12008  fsumabs  12016  fprodcllemf  12164  fprod2dlemstep  12173  fprodcnv  12176  fprodcom2fi  12177  fprodmodd  12192  4sqleminfi  12960  ennnfonelemim  13035  topnfn  13317  ptex  13337  prdsvallem  13345  prdsval  13346  xpsff1o  13422  ismgm  13430  issgrp  13476  ismnddef  13491  isnsg  13779  fnmgp  13925  isrng  13937  isring  14003  dfrhm2  14158  znval  14640  iuncld  14829  txbas  14972  txdis  14991  xmetunirn  15072  xmettxlem  15223  xmettx  15224  gausslemma2dlem1a  15777  isuhgrm  15912  isushgrm  15913  isupgren  15936  upgrex  15944  isumgren  15946  isuspgren  15996  isusgren  15997  vtxdgfval  16094  clwwlknon  16224  pw1nct  16540