Theorem elv 2825

Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2824), 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 2824	. 2 ⊢ 𝑥 ∈ V
2		elv.1	. 2 ⊢ (𝑥 ∈ V → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2209  Vcvv 2821

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  xpiindim  4912  disjxp1  6462  cnvimadfsn  6475  ixpiinm  6996  ixpsnf1o  7008  modom  7098  eqsndc  7200  iunfidisj  7250  ssfii  7298  fifo  7304  dcfi  7305  omp1eomlem  7424  exmidomniim  7471  bcval5  11179  hashmap  11246  hashfibclem  11260  hashf1lem2  11264  hashf1  11265  rexfiuz  11733  fsum2dlemstep  12179  fsumcnv  12182  fisumcom2  12183  fsumconst  12199  modfsummodlemstep  12202  fsumabs  12210  fprodcllemf  12358  fprod2dlemstep  12367  fprodcnv  12370  fprodcom2fi  12371  fprodmodd  12386  4sqleminfi  13154  ennnfonelemim  13293  topnfn  13575  ptex  13595  prdsvallem  13598  xpsff1o  13647  ismgm  13654  issgrp  13695  ismnddef  13708  isnsg  13982  gsumconstcmn  14143  prdsval  14150  fnmgp  14196  isrng  14208  isring  14278  dfrhm2  14434  znval  14943  iuncld  15139  txbas  15282  txdis  15301  xmetunirn  15382  xmettxlem  15533  xmettx  15534  logfac  15918  gausslemma2dlem1a  16091  isuhgrm  16226  isushgrm  16227  isupgren  16250  upgrex  16258  isumgren  16260  isuspgren  16312  isusgren  16313  vtxdgfval  16443  clwwlknon  16584  pw1nct  16947