Theorem elv 3498

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495

This theorem is referenced by:  csbvarg  4381  iinconst  4920  iuniin  4922  iinssiun  4923  iinss1  4925  ssiinf  4969  iinss  4971  iinss2  4972  iinab  4981  iinun2  4986  iundif2  4987  iindif1  4988  iindif2  4990  iinin2  4991  iinpw  5019  brab1  5105  triin  5178  eusvnf  5283  sbcop  5371  pwvabrel  5596  difopab  5695  xpiindi  5699  dmopab2rex  5779  dfima2  5924  args  5950  inisegn0  5954  dffr3  5955  dfse2  5956  dfco2a  6092  iotaval  6322  iinpreima  6830  tfinds2  7570  fvresex  7653  fnse  7819  suppvalbr  7826  cnvimadfsn  7831  reldmtpos  7892  rntpos  7897  ovtpos  7899  dftpos3  7902  tpostpos  7904  wfrlem10  7956  onovuni  7971  oarec  8180  eqerlem  8315  ixpiin  8480  ixpsnf1o  8494  boxriin  8496  idssen  8546  unxpdomlem3  8716  ac6sfi  8754  unbnn2  8767  fifo  8888  inf0  9076  rankxpsuc  9303  tcrank  9305  harcard  9399  infxpenlem  9431  infpwfien  9480  alephcard  9488  dfac3  9539  cflm  9664  fin23lem34  9760  dffin7-2  9812  fin1a2lem13  9826  itunitc1  9834  itunitc  9835  ituniiun  9836  hsmexlem4  9843  fin41  9858  axdclem2  9934  fpwwe2lem12  10055  fpwwe2lem13  10056  fpwwe2  10057  canthwe  10065  pwfseqlem5  10077  axgroth2  10239  axgroth6  10242  grothac  10244  grothtsk  10249  seqfeq4  13411  serle  13417  seqof  13419  hash1snb  13772  hashmap  13788  hashfun  13790  hashbclem  13802  hashf1lem2  13806  hashf1  13807  hash2prde  13820  prprrab  13823  fi1uzind  13847  s3sndisj  14319  s3iunsndisj  14320  rexfiuz  14699  fsumabs  15148  incexclem  15183  fprodcllemf  15304  fprodmodd  15343  iserodd  16164  hashbc0  16333  0ram  16348  ramub1  16356  initoid  17257  termoid  17258  equivestrcsetc  17394  gsumwspan  18003  gsmsymgrfix  18548  symgfixf1  18557  frgpnabllem1  18985  telgsums  19105  opprsubg  19378  subrgpropd  19562  coe1fzgsumdlem  20461  evl1gsumdlem  20511  mdetunilem9  21221  topnex  21596  neitr  21780  ordtbas2  21791  pnfnei  21820  mnfnei  21821  hauscmplem  22006  2ndcsb  22049  2ndcsep  22059  ptpjopn  22212  snfil  22464  fbasrn  22484  rnelfmlem  22552  rnelfm  22553  fmfnfmlem3  22556  fmfnfmlem4  22557  fmfnfm  22558  fclscmp  22630  alexsubALTlem4  22650  ptcmplem2  22653  symgtgp  22706  ustfilxp  22813  restutopopn  22839  ustuqtop2  22843  utopsnneiplem  22848  imasdsf1olem  22975  xpsdsval  22983  metuel2  23167  metustbl  23168  restmetu  23172  xrtgioo  23406  minveclem3b  24023  ovoliunlem1  24095  uniioombllem3  24178  itg1addlem4  24292  dvnff  24512  dvfsumlem3  24617  logfac  25176  gausslemma2dlem1a  25933  umgrislfupgrlem  26899  lfuhgr1v0e  27028  cplgrop  27211  finsumvtxdg2size  27324  rgrusgrprc  27363  elwspths2spth  27738  fusgr2wsp2nb  28105  h2hlm  28749  axhcompl-zf  28767  opsbc2ie  30231  inpr0  30284  iuninc  30304  disjpreima  30326  suppss2f  30376  fnpreimac  30408  tocyccntz  30779  esumpfinvalf  31328  measiuns  31469  bnj23  31981  bnj110  32123  bnj1123  32251  bnj1373  32295  lfuhgr2  32358  lfuhgr3  32359  acycgr1v  32389  umgracycusgr  32394  cusgracyclt3v  32396  dmopab3rexdif  32645  dfpo2  32984  wzel  33104  fprlem2  33131  dfrdg4  33405  bj-sbeq  34211  bj-sbel1  34215  bj-snsetex  34268  bj-snglc  34274  bj-taginv  34291  eldmres  35522  ecres  35527  ecres2  35528  eldmqsres  35535  inxprnres  35541  cnvepres  35547  idinxpss  35562  inxpssidinxp  35565  idinxpssinxp  35566  alrmomorn  35604  alrmomodm  35605  brxrn  35618  dfxrn2  35620  inxpxrn  35635  rnxrn  35638  rnxrnres  35639  rnxrncnvepres  35640  rnxrnidres  35641  1cossres  35666  dfcoels  35667  br1cossinidres  35681  br1cossincnvepres  35682  br1cossxrnidres  35683  br1cossxrncnvepres  35684  refrelcosslem  35694  coss0  35711  cossid  35712  br1cossxrncnvssrres  35740  dfrefrels2  35745  dfcnvrefrels2  35758  dfcnvrefrels3  35759  dfsymrels2  35773  dftrrels2  35803  eldmqs1cossres  35885  dfeldisj5  35946  prter2  36009  cdleme31sdnN  37515  inintabss  39928  inintabd  39929  cnvcnvintabd  39950  cnvintabd  39953  comptiunov2i  40041  cotrcltrcl  40060  corcltrcl  40074  cotrclrcl  40077  rr-grothprimbi  40621  rr-groth  40625  onfrALTlem4VD  41210  iinssiin  41384  iinssf  41396  rnmptpr  41422  wessf1ornlem  41434  rnmptlb  41503  rnmptbddlem  41504  rnmptbd2lem  41509  ellimcabssub0  41887  eusnsn  43251  dfdfat2  43317  onsetreclem1  44797