Theorem elv 2807

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

Syntax hints:   → wi 4   ∈ wcel 2202  Vcvv 2803

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 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805

This theorem is referenced by:  xpiindim  4873  disjxp1  6410  cnvimadfsn  6423  ixpiinm  6936  ixpsnf1o  6948  modom  7037  eqsndc  7138  iunfidisj  7188  ssfii  7216  fifo  7222  dcfi  7223  omp1eomlem  7336  exmidomniim  7383  bcval5  11071  rexfiuz  11612  fsum2dlemstep  12058  fsumcnv  12061  fisumcom2  12062  fsumconst  12078  modfsummodlemstep  12081  fsumabs  12089  fprodcllemf  12237  fprod2dlemstep  12246  fprodcnv  12249  fprodcom2fi  12250  fprodmodd  12265  4sqleminfi  13033  ennnfonelemim  13108  topnfn  13390  ptex  13410  prdsvallem  13418  prdsval  13419  xpsff1o  13495  ismgm  13503  issgrp  13549  ismnddef  13564  isnsg  13852  fnmgp  13999  isrng  14011  isring  14077  dfrhm2  14232  znval  14715  iuncld  14909  txbas  15052  txdis  15071  xmetunirn  15152  xmettxlem  15303  xmettx  15304  gausslemma2dlem1a  15860  isuhgrm  15995  isushgrm  15996  isupgren  16019  upgrex  16027  isumgren  16029  isuspgren  16081  isusgren  16082  vtxdgfval  16212  clwwlknon  16353  pw1nct  16708