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 ⊢ 𝜑

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  Vcvv 2821

This proof depends on 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 proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  xpiindim  4917  disjxp1  6472  cnvimadfsn  6485  ixpiinm  7006  ixpsnf1o  7018  modom  7108  eqsndc  7210  iunfidisj  7260  ssfii  7308  fifo  7314  dcfi  7315  omp1eomlem  7435  exmidomniim  7482  bcval5  11217  hashmap  11284  hashfibclem  11298  hashf1lem2  11302  hashf1  11303  rexfiuz  11771  fiidxsupcl  12012  fsum2dlemstep  12220  fsumcnv  12223  fisumcom2  12224  fsumconst  12240  modfsummodlemstep  12243  fsumabs  12251  fprodcllemf  12399  fprod2dlemstep  12408  fprodcnv  12411  fprodcom2fi  12412  fprodmodd  12427  4sqleminfi  13199  ennnfonelemim  13367  topnfn  13651  ptex  13671  prdsvallem  13674  xpsff1o  13723  ismgm  13730  issgrp  13771  ismnddef  13784  isnsg  14058  gsumconstcmn  14250  prdsval  14257  fnmgp  14303  isrng  14317  isring  14388  dfrhm2  14545  znval  15055  iuncld  15307  txbas  15450  txdis  15469  xmetunirn  15550  xmettxlem  15701  xmettx  15702  logfac  16090  gausslemma2dlem1a  16343  isuhgrm  16478  isushgrm  16479  isupgren  16502  upgrex  16510  isumgren  16512  isuspgren  16564  isusgren  16565  vtxdgfval  16695  clwwlknon  16836  pw1nct  17199