Theorem elv 2716

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

Syntax hints:   → wi 4   ∈ wcel 2128  Vcvv 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-v 2714

This theorem is referenced by:  xpiindim  4720  disjxp1  6177  ixpiinm  6662  ixpsnf1o  6674  iunfidisj  6883  ssfii  6911  fifo  6917  omp1eomlem  7028  exmidomniim  7067  bcval5  10619  rexfiuz  10871  fsum2dlemstep  11313  fsumcnv  11316  fisumcom2  11317  fsumconst  11333  modfsummodlemstep  11336  fsumabs  11344  fprodcllemf  11492  fprod2dlemstep  11501  fprodcnv  11504  fprodcom2fi  11505  fprodmodd  11520  ennnfonelemim  12125  topnfn  12316  iuncld  12475  txbas  12618  txdis  12637  xmetunirn  12718  xmettxlem  12869  xmettx  12870  pw1nct  13535