Theorem elv 2819

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

Syntax hints:   → wi 4   ∈ wcel 2205  Vcvv 2815

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 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  xpiindim  4897  disjxp1  6445  cnvimadfsn  6458  ixpiinm  6972  ixpsnf1o  6984  modom  7074  eqsndc  7176  iunfidisj  7226  ssfii  7274  fifo  7280  dcfi  7281  omp1eomlem  7398  exmidomniim  7445  bcval5  11150  hashmap  11217  hashfibclem  11231  rexfiuz  11699  fsum2dlemstep  12145  fsumcnv  12148  fisumcom2  12149  fsumconst  12165  modfsummodlemstep  12168  fsumabs  12176  fprodcllemf  12324  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  fprodmodd  12352  4sqleminfi  13120  ennnfonelemim  13259  topnfn  13541  ptex  13561  prdsvallem  13564  xpsff1o  13613  ismgm  13620  issgrp  13666  ismnddef  13679  isnsg  13955  prdsval  14115  fnmgp  14161  isrng  14173  isring  14243  dfrhm2  14399  znval  14910  iuncld  15106  txbas  15249  txdis  15268  xmetunirn  15349  xmettxlem  15500  xmettx  15501  gausslemma2dlem1a  16057  isuhgrm  16192  isushgrm  16193  isupgren  16216  upgrex  16224  isumgren  16226  isuspgren  16278  isusgren  16279  vtxdgfval  16409  clwwlknon  16550  pw1nct  16903