Theorem elv 3455

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  csbconstg  3866  csbvarg  4392  iinconst  4962  iuniin  4964  iinssiun  4965  iinss1  4967  ssiinf  5013  iinss  5015  iinss2  5016  iinab  5026  iinun2  5031  iundif2  5032  iindif1  5035  iindif2  5037  iinin2  5038  iinpw  5066  brab1  5153  triin  5229  eusvnf  5357  sbcop  5465  iunopab  5538  pwvabrel  5706  ssrel  5763  xpiindi  5815  cnv0  5863  dmopab2rex  5901  dfima2  6058  args  6088  inisegn0  6094  dffr3  6095  dfse2  6096  dfco2a  6242  dfpo2  6294  iotaval2  6504  iinpreima  7063  tfinds2  7861  fvresex  7958  sbcoteq1a  8049  fnse  8132  xpord2pred  8144  xpord3lem  8148  xpord3pred  8151  suppvalbr  8163  cnvimadfsn  8171  reldmtpos  8233  rntpos  8238  ovtpos  8240  dftpos3  8243  tpostpos  8245  fprlem2  8301  onovuni  8332  oarec  8550  eqerlem  8733  elecreseq  8747  ixpiin  8932  ixpsnf1o  8946  boxriin  8948  idssen  9004  unxpdomlem3  9229  ac6sfi  9255  unbnn2  9268  fifo  9403  inf0  9601  ttrclselem2  9706  ttrclse  9707  rankxpsuc  9865  tcrank  9867  harcard  9984  infxpenlem  10017  infpwfien  10066  alephcard  10074  dfac3  10125  cflm  10252  fin23lem34  10349  dffin7-2  10401  fin1a2lem13  10415  itunitc1  10423  itunitc  10424  ituniiun  10425  hsmexlem4  10432  fin41  10447  axdclem2  10523  fpwwe2lem11  10651  fpwwe2lem12  10652  fpwwe2  10653  canthwe  10661  pwfseqlem5  10673  axgroth2  10835  axgroth6  10838  grothac  10840  grothtsk  10845  seqfeq4  14116  serle  14122  seqof  14124  hash1snb  14485  hashmap  14501  hashfun  14503  hashbclem  14518  hashf1lem2  14522  hashf1  14523  hash2prde  14536  prprrab  14539  hash3tpexb  14560  fi1uzind  14573  brfi1indALT  14576  s3sndisj  15041  s3iunsndisj  15042  rexfiuz  15436  fsumabs  15889  incexclem  15926  fprodcllemf  16046  fprodmodd  16085  iserodd  16928  hashbc0  17098  0ram  17113  ramub1  17121  initoid  18091  termoid  18092  equivestrcsetc  18241  gsumwspan  18956  gsmsymgrfix  19556  symgfixf1  19565  frgpnabllem1  20001  telgsums  20121  opprsubg  20494  subrngpropd  20731  subrgpropd  20771  coe1fzgsumdlem  22529  evl1gsumdlem  22582  mdetunilem9  22843  topnex  23222  neitr  23406  ordtbas2  23417  pnfnei  23446  mnfnei  23447  hauscmplem  23632  2ndcsb  23675  2ndcsep  23686  ptpjopn  23839  snfil  24091  fbasrn  24111  rnelfmlem  24179  rnelfm  24180  fmfnfmlem3  24183  fmfnfmlem4  24184  fmfnfm  24185  fclscmp  24257  alexsubALTlem4  24277  ptcmplem2  24280  symgtgp  24333  ustfilxp  24440  restutopopn  24465  ustuqtop2  24469  utopsnneiplem  24474  imasdsf1olem  24600  xpsdsval  24608  metuel2  24792  metustbl  24793  restmetu  24797  xrtgioo  25034  minveclem3b  25657  ovoliunlem1  25731  uniioombllem3  25814  itg1addlem4  25928  dvnff  26151  dvfsumlem3  26256  logfac  26839  gausslemma2dlem1a  27602  onsis  28540  ons2ind  28541  umgrislfupgrlem  29580  lfuhgr2  29607  lfuhgr3  29608  lfuhgr1v0e  29715  cplgrop  29898  finsumvtxdg2size  30011  rgrusgrprc  30050  elwspths2spth  30439  fusgr2wsp2nb  30815  h2hlm  31462  axhcompl-zf  31480  opsbc2ie  32952  inpr0  33008  iuninc  33035  disjpreima  33058  suppss2f  33112  fnpreimac  33144  tocyccntz  33585  elrgspnlem1  33683  elrgspnlem2  33684  nsgqusf1olem2  33844  nsgqusf1olem3  33845  zarclsiin  34382  esumpfinvalf  34587  measiuns  34729  bnj23  35229  bnj110  35368  bnj1123  35496  bnj1373  35540  fineqvnttrclse  35651  kardeq0  35683  acycgr1v  35729  umgracycusgr  35734  cusgracyclt3v  35736  dmopab3rexdif  35985  wzel  36402  dfrdg4  36531  bj-sbeq  37645  bj-sbel1  37649  bj-snsetex  37708  bj-snglc  37714  bj-taginv  37731  bj-adjfrombun  37791  poimirlem16  38386  poimirlem19  38389  findcard4  38464  eldmres  39026  ecres  39034  eldmqsres  39042  inxprnres  39047  cnvepres  39053  idinxpss  39067  inxpssidinxp  39071  idinxpssinxp  39072  cnvref5  39100  alrmomorn  39107  alrmomodm  39108  ssdmral  39128  brxrn  39132  dfxrn2  39134  dmcnvep  39137  inxpxrn  39167  rnxrn  39170  rnxrnres  39171  rnxrncnvepres  39172  rnxrnidres  39173  blockadjliftmap  39207  dfsucmap3  39212  dmsucmap  39217  dfsuccl4  39223  coss1cnvres  39256  coss2cnvepres  39257  1cossres  39268  dfcoels  39269  refressn  39282  br1cossinidres  39288  br1cossincnvepres  39289  br1cossxrnidres  39290  br1cossxrncnvepres  39291  refrelcosslem  39301  coss0  39318  cossid  39319  br1cossxrncnvssrres  39337  dfrefrels2  39342  dfcnvrefrels2  39357  dfcnvrefrels3  39358  dfsymrels2  39374  dftrrels2  39408  eldmqs1cossres  39493  disjimdmqseq  39558  dfeldisj5  39562  eldisjdmqsim  39566  disjres  39593  antisymrelres  39615  disjdmqsss  39654  disjdmqscossss  39655  mpets  39705  dmqsblocks  39716  dfpeters2  39723  prter2  39755  cdleme31sdnN  41261  evl1gprodd  42984  sn-iotalem  43092  inintabss  44419  inintabd  44420  cnvcnvintabd  44441  cnvintabd  44444  comptiunov2i  44547  cotrcltrcl  44566  corcltrcl  44580  cotrclrcl  44583  rr-grothprimbi  45120  rr-groth  45124  dfuniv2  45127  onfrALTlem4VD  45709  iinssiin  45962  iinssf  45971  iindif2f  45993  rnmptpr  46010  wessf1ornlem  46018  disjinfi  46025  rnmptlb  46073  rnmptbddlem  46074  rnmptbd2lem  46078  ellimcabssub0  46448  preimageiingt  47549  preimaleiinlt  47550  eusnsn  47915  dfdfat2  48017  iineq0  49749  iinxp  49760  mofeu  49777  tposres0  49804  iinfsubc  49985  onsetreclem1  50632