Theorem elv 2817

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

Syntax hints:   → wi 4   ∈ wcel 2203  Vcvv 2813

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  xpiindim  4892  disjxp1  6432  cnvimadfsn  6445  ixpiinm  6959  ixpsnf1o  6971  modom  7061  eqsndc  7163  iunfidisj  7213  ssfii  7261  fifo  7267  dcfi  7268  omp1eomlem  7385  exmidomniim  7432  bcval5  11125  hashmap  11192  hashfibclem  11206  rexfiuz  11674  fsum2dlemstep  12120  fsumcnv  12123  fisumcom2  12124  fsumconst  12140  modfsummodlemstep  12143  fsumabs  12151  fprodcllemf  12299  fprod2dlemstep  12308  fprodcnv  12311  fprodcom2fi  12312  fprodmodd  12327  4sqleminfi  13095  ennnfonelemim  13175  topnfn  13457  ptex  13477  prdsvallem  13485  prdsval  13486  xpsff1o  13562  ismgm  13570  issgrp  13616  ismnddef  13631  isnsg  13919  fnmgp  14066  isrng  14078  isring  14144  dfrhm2  14299  znval  14784  iuncld  14980  txbas  15123  txdis  15142  xmetunirn  15223  xmettxlem  15374  xmettx  15375  gausslemma2dlem1a  15931  isuhgrm  16066  isushgrm  16067  isupgren  16090  upgrex  16098  isumgren  16100  isuspgren  16152  isusgren  16153  vtxdgfval  16283  clwwlknon  16424  pw1nct  16777