Theorem elv 2741

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

Syntax hints:   → wi 4   ∈ wcel 2148  Vcvv 2737

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739

This theorem is referenced by:  xpiindim  4764  disjxp1  6236  ixpiinm  6723  ixpsnf1o  6735  iunfidisj  6944  ssfii  6972  fifo  6978  dcfi  6979  omp1eomlem  7092  exmidomniim  7138  bcval5  10738  rexfiuz  10993  fsum2dlemstep  11437  fsumcnv  11440  fisumcom2  11441  fsumconst  11457  modfsummodlemstep  11460  fsumabs  11468  fprodcllemf  11616  fprod2dlemstep  11625  fprodcnv  11628  fprodcom2fi  11629  fprodmodd  11644  ennnfonelemim  12419  topnfn  12683  ismgm  12730  issgrp  12763  ismnddef  12773  isnsg  13015  fnmgp  13085  isring  13136  iuncld  13508  txbas  13651  txdis  13670  xmetunirn  13751  xmettxlem  13902  xmettx  13903  pw1nct  14634