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  7012  ixpsnf1o  7024  modom  7114  eqsndc  7216  iunfidisj  7266  relresfin  7270  ssfii  7313  fifo  7319  dcfi  7320  omp1eomlem  7440  exmidomniim  7487  bcval5  11222  hashmap  11289  hashfibclem  11303  hashf1lem2  11307  hashf1  11308  rexfiuz  11776  fiidxsupcl  12017  fsum2dlemstep  12225  fsumcnv  12228  fisumcom2  12229  fsumconst  12245  modfsummodlemstep  12248  fsumabs  12256  fprodcllemf  12404  fprod2dlemstep  12413  fprodcnv  12416  fprodcom2fi  12417  fprodmodd  12432  4sqleminfi  13204  ennnfonelemim  13372  topnfn  13656  ptex  13676  prdsvallem  13679  xpsff1o  13728  ismgm  13735  issgrp  13776  ismnddef  13789  isnsg  14063  gsumconstcmn  14265  gsum2d2fi  14273  prdsval  14279  fnmgp  14325  isrng  14339  isring  14410  dfrhm2  14569  znval  15079  psrbagmaxlem1  15178  psrridmfi  15209  iuncld  15358  txbas  15501  txdis  15520  xmetunirn  15601  xmettxlem  15752  xmettx  15753  logfac  16143  gausslemma2dlem1a  16399  isuhgrm  16534  isushgrm  16535  isupgren  16558  upgrex  16566  isumgren  16568  isuspgren  16620  isusgren  16621  vtxdgfval  16751  clwwlknon  16892  pw1nct  17255