Theorem elv 2742

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

Syntax hints:   → wi 4   ∈ wcel 2148  Vcvv 2738

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 2740

This theorem is referenced by:  xpiindim  4765  disjxp1  6237  ixpiinm  6724  ixpsnf1o  6736  iunfidisj  6945  ssfii  6973  fifo  6979  dcfi  6980  omp1eomlem  7093  exmidomniim  7139  bcval5  10743  rexfiuz  10998  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  fsumconst  11462  modfsummodlemstep  11465  fsumabs  11473  fprodcllemf  11621  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodmodd  11649  ennnfonelemim  12425  topnfn  12693  ptex  12713  xpsff1o  12768  ismgm  12776  issgrp  12809  ismnddef  12819  isnsg  13062  fnmgp  13132  isring  13183  iuncld  13618  txbas  13761  txdis  13780  xmetunirn  13861  xmettxlem  14012  xmettx  14013  pw1nct  14755