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  4919  disjxp1  6476  cnvimadfsn  6489  ixpiinm  7010  ixpsnf1o  7022  modom  7112  eqsndc  7214  iunfidisj  7264  relresfin  7268  ssfii  7313  fifo  7319  dcfi  7320  omp1eomlem  7440  exmidomniim  7487  bcval5  11223  hashmap  11290  hashfibclem  11304  hashf1lem2  11308  hashf1  11309  rexfiuz  11777  fiidxsupcl  12018  fsum2dlemstep  12226  fsumcnv  12229  fisumcom2  12230  fsumconst  12246  modfsummodlemstep  12249  fsumabs  12257  fprodcllemf  12405  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  fprodmodd  12433  4sqleminfi  13205  ennnfonelemim  13373  topnfn  13657  ptex  13677  prdsvallem  13680  xpsff1o  13729  ismgm  13736  issgrp  13777  ismnddef  13790  isnsg  14064  gsumconstcmn  14266  gsum2d2fi  14274  prdsval  14280  fnmgp  14326  isrng  14340  isring  14411  dfrhm2  14570  znval  15080  psrridmfi  15200  iuncld  15341  txbas  15484  txdis  15503  xmetunirn  15584  xmettxlem  15735  xmettx  15736  logfac  16126  gausslemma2dlem1a  16382  isuhgrm  16517  isushgrm  16518  isupgren  16541  upgrex  16549  isumgren  16551  isuspgren  16603  isusgren  16604  vtxdgfval  16734  clwwlknon  16875  pw1nct  17238