Theorem elv 3469

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466

This theorem is referenced by:  csbconstg  3898  csbvarg  4414  iinconst  4983  iuniin  4985  iinssiun  4986  iinss1  4988  ssiinf  5035  iinss  5037  iinss2  5038  iinab  5049  iinun2  5054  iundif2  5055  iindif1  5056  iindif2  5058  iinin2  5059  iinpw  5087  brab1  5172  triin  5251  eusvnf  5367  sbcop  5469  iunopab  5539  pwvabrel  5710  ssrel  5766  difopabOLD  5815  xpiindi  5820  dmopab2rex  5902  dfima2  6054  args  6084  inisegn0  6090  dffr3  6091  dfse2  6092  dfco2a  6240  dfpo2  6290  iotaval2  6504  iotavalOLD  6510  iinpreima  7064  tfinds2  7864  fvresex  7963  sbcoteq1a  8055  fnse  8137  xpord2pred  8149  xpord3lem  8153  xpord3pred  8156  suppvalbr  8168  cnvimadfsn  8176  reldmtpos  8238  rntpos  8243  ovtpos  8245  dftpos3  8248  tpostpos  8250  fprlem2  8305  wfrlem10OLD  8337  onovuni  8361  oarec  8579  eqerlem  8759  ixpiin  8943  ixpsnf1o  8957  boxriin  8959  idssen  9016  unxpdomlem3  9265  ac6sfi  9297  unbnn2  9310  fifo  9449  inf0  9640  ttrclselem2  9745  ttrclse  9746  rankxpsuc  9901  tcrank  9903  harcard  9997  infxpenlem  10032  infpwfien  10081  alephcard  10089  dfac3  10140  cflm  10269  fin23lem34  10365  dffin7-2  10417  fin1a2lem13  10431  itunitc1  10439  itunitc  10440  ituniiun  10441  hsmexlem4  10448  fin41  10463  axdclem2  10539  fpwwe2lem11  10660  fpwwe2lem12  10661  fpwwe2  10662  canthwe  10670  pwfseqlem5  10682  axgroth2  10844  axgroth6  10847  grothac  10849  grothtsk  10854  seqfeq4  14074  serle  14080  seqof  14082  hash1snb  14442  hashmap  14458  hashfun  14460  hashbclem  14475  hashf1lem2  14479  hashf1  14480  hash2prde  14493  prprrab  14496  hash3tpexb  14517  fi1uzind  14530  brfi1indALT  14533  s3sndisj  14991  s3iunsndisj  14992  rexfiuz  15371  fsumabs  15822  incexclem  15857  fprodcllemf  15979  fprodmodd  16018  iserodd  16860  hashbc0  17030  0ram  17045  ramub1  17053  initoid  18019  termoid  18020  equivestrcsetc  18169  gsumwspan  18829  gsmsymgrfix  19414  symgfixf1  19423  frgpnabllem1  19859  telgsums  19979  opprsubg  20317  subrngpropd  20533  subrgpropd  20573  coe1fzgsumdlem  22246  evl1gsumdlem  22299  mdetunilem9  22563  topnex  22939  neitr  23123  ordtbas2  23134  pnfnei  23163  mnfnei  23164  hauscmplem  23349  2ndcsb  23392  2ndcsep  23402  ptpjopn  23555  snfil  23807  fbasrn  23827  rnelfmlem  23895  rnelfm  23896  fmfnfmlem3  23899  fmfnfmlem4  23900  fmfnfm  23901  fclscmp  23973  alexsubALTlem4  23993  ptcmplem2  23996  symgtgp  24049  ustfilxp  24156  restutopopn  24182  ustuqtop2  24186  utopsnneiplem  24191  imasdsf1olem  24317  xpsdsval  24325  metuel2  24509  metustbl  24510  restmetu  24514  xrtgioo  24751  minveclem3b  25385  ovoliunlem1  25460  uniioombllem3  25543  itg1addlem4  25657  dvnff  25882  dvfsumlem3  25992  logfac  26567  gausslemma2dlem1a  27333  onsis  28229  umgrislfupgrlem  29106  lfuhgr1v0e  29238  cplgrop  29421  finsumvtxdg2size  29535  rgrusgrprc  29574  elwspths2spth  29954  fusgr2wsp2nb  30320  h2hlm  30966  axhcompl-zf  30984  opsbc2ie  32462  inpr0  32518  iuninc  32546  disjpreima  32570  suppss2f  32621  fnpreimac  32654  tocyccntz  33160  elrgspnlem1  33242  elrgspnlem2  33243  nsgqusf1olem2  33434  nsgqusf1olem3  33435  zarclsiin  33907  esumpfinvalf  34112  measiuns  34253  bnj23  34754  bnj110  34894  bnj1123  35022  bnj1373  35066  lfuhgr2  35146  lfuhgr3  35147  acycgr1v  35176  umgracycusgr  35181  cusgracyclt3v  35183  dmopab3rexdif  35432  wzel  35847  dfrdg4  35974  bj-sbeq  36924  bj-sbel1  36928  bj-snsetex  36986  bj-snglc  36992  bj-taginv  37009  bj-adjfrombun  37069  poimirlem16  37665  poimirlem19  37668  eldmres  38293  ecres  38301  ecres2  38302  eldmqsres  38310  inxprnres  38315  cnvepres  38321  idinxpss  38335  inxpssidinxp  38339  idinxpssinxp  38340  cnvref5  38374  alrmomorn  38381  alrmomodm  38382  brxrn  38397  dfxrn2  38399  inxpxrn  38418  rnxrn  38421  rnxrnres  38422  rnxrncnvepres  38423  rnxrnidres  38424  coss1cnvres  38440  coss2cnvepres  38441  1cossres  38452  dfcoels  38453  refressn  38466  br1cossinidres  38472  br1cossincnvepres  38473  br1cossxrnidres  38474  br1cossxrncnvepres  38475  refrelcosslem  38485  coss0  38502  cossid  38503  br1cossxrncnvssrres  38531  dfrefrels2  38536  dfcnvrefrels2  38551  dfcnvrefrels3  38552  dfsymrels2  38568  dftrrels2  38598  eldmqs1cossres  38682  dfeldisj5  38744  disjres  38767  antisymrelres  38786  disjdmqsss  38825  disjdmqscossss  38826  mpets  38865  prter2  38904  cdleme31sdnN  40411  evl1gprodd  42135  sn-iotalem  42239  inintabss  43577  inintabd  43578  cnvcnvintabd  43599  cnvintabd  43602  comptiunov2i  43705  cotrcltrcl  43724  corcltrcl  43738  cotrclrcl  43741  rr-grothprimbi  44294  rr-groth  44298  dfuniv2  44301  onfrALTlem4VD  44885  iinssiin  45133  iinssf  45142  iindif2f  45164  rnmptpr  45181  wessf1ornlem  45189  disjinfi  45196  rnmptlb  45247  rnmptbddlem  45248  rnmptbd2lem  45252  ellimcabssub0  45626  eusnsn  47035  dfdfat2  47137  iineq0  48778  iinxp  48789  mofeu  48806  tposres0  48832  iinfsubc  49005  onsetreclem1  49549