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  7434  exmidomniim  7481  bcval5  11201  hashmap  11268  hashfibclem  11282  hashf1lem2  11286  hashf1  11287  rexfiuz  11755  fsum2dlemstep  12201  fsumcnv  12204  fisumcom2  12205  fsumconst  12221  modfsummodlemstep  12224  fsumabs  12232  fprodcllemf  12380  fprod2dlemstep  12389  fprodcnv  12392  fprodcom2fi  12393  fprodmodd  12408  4sqleminfi  13176  ennnfonelemim  13315  topnfn  13598  ptex  13618  prdsvallem  13621  xpsff1o  13670  ismgm  13677  issgrp  13718  ismnddef  13731  isnsg  14005  gsumconstcmn  14166  prdsval  14173  fnmgp  14219  isrng  14233  isring  14304  dfrhm2  14461  znval  14971  iuncld  15216  txbas  15359  txdis  15378  xmetunirn  15459  xmettxlem  15610  xmettx  15611  logfac  15995  gausslemma2dlem1a  16177  isuhgrm  16312  isushgrm  16313  isupgren  16336  upgrex  16344  isumgren  16346  isuspgren  16398  isusgren  16399  vtxdgfval  16529  clwwlknon  16670  pw1nct  17033