Theorem elv 3459

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  csbconstg  3870  csbvarg  4395  iinconst  4967  iuniin  4969  iinssiun  4970  iinss1  4972  ssiinf  5018  iinss  5020  iinss2  5021  iinab  5031  iinun2  5036  iundif2  5037  iindif1  5040  iindif2  5042  iinin2  5043  iinpw  5071  brab1  5159  triin  5235  eusvnf  5361  sbcop  5466  iunopab  5541  pwvabrel  5709  ssrelOLD  5768  xpiindi  5822  cnv0  5873  dmopab2rex  5911  dfima2  6076  args  6108  inisegn0  6114  dffr3  6115  dfse2  6116  dfco2a  6266  dfpo2  6325  iotaval2  6535  iinpreima  7101  tfinds2  7909  fvresex  8006  sbcoteq1a  8097  fnse  8187  xpord2pred  8199  xpord3lem  8203  xpord3pred  8206  suppvalbr  8218  suppvalbrOLD  8219  cnvimadfsn  8227  reldmtpos  8289  rntpos  8294  ovtpos  8296  dftpos3  8299  tpostpos  8301  fprlem2  8357  onovuni  8388  oarec  8608  eqerlem  8791  elecreseq  8805  ixpiin  8990  ixpsnf1o  9004  boxriin  9006  idssen  9062  unxpdomlem3  9287  ac6sfi  9313  unbnn2  9327  fifo  9461  inf0  9659  ttrclselem2  9764  ttrclse  9765  rankxpsuc  9936  tcrank  9938  harcard  10096  infxpenlem  10131  infpwfien  10180  alephcard  10188  dfac3  10239  cflm  10366  fin23lem34  10463  dffin7-2  10515  fin1a2lem13  10529  itunitc1  10537  itunitc  10538  ituniiun  10539  hsmexlem4  10546  fin41  10561  axdclem2  10637  fpwwe2lem11  10765  fpwwe2lem12  10766  fpwwe2  10767  canthwe  10775  pwfseqlem5  10787  axgroth2  10949  axgroth6  10952  grothac  10954  grothtsk  10959  seqfeq4  14234  serle  14240  seqof  14242  hash1snb  14605  hashmap  14621  hashfun  14623  hashbclem  14638  hashf1lem2  14642  hashf1  14643  hash2prde  14656  prprrab  14659  hash3tpexb  14680  fi1uzind  14693  brfi1indALT  14696  s3sndisj  15163  s3iunsndisj  15164  rexfiuz  15559  fsumabs  16012  incexclem  16049  fprodcllemf  16169  fprodmodd  16208  iserodd  17057  hashbc0  17227  0ram  17242  ramub1  17250  initoid  18226  termoid  18227  equivestrcsetc  18376  gsumwspan  19092  gsmsymgrfix  19693  symgfixf1  19702  frgpnabllem1  20138  telgsums  20258  opprsubg  20633  subrngpropd  20871  subrgpropd  20911  coe1fzgsumdlem  22676  evl1gsumdlem  22729  mdetunilem9  22990  topnex  23369  neitr  23553  ordtbas2  23564  pnfnei  23593  mnfnei  23594  hauscmplem  23779  2ndcsb  23822  2ndcsep  23833  ptpjopn  23986  snfil  24238  fbasrn  24258  rnelfmlem  24326  rnelfm  24327  fmfnfmlem3  24330  fmfnfmlem4  24331  fmfnfm  24332  fclscmp  24404  alexsubALTlem4  24424  ptcmplem2  24427  symgtgp  24480  ustfilxp  24587  restutopopn  24612  ustuqtop2  24616  utopsnneiplem  24621  imasdsf1olem  24747  xpsdsval  24755  metuel2  24939  metustbl  24940  restmetu  24944  xrtgioo  25181  minveclem3b  25804  ovoliunlem1  25878  uniioombllem3  25961  itg1addlem4  26075  dvnff  26298  dvfsumlem3  26403  logfac  26986  gausslemma2dlem1a  27749  onsis  28717  ons2ind  28718  umgrislfupgrlem  29757  lfuhgr2  29784  lfuhgr3  29785  lfuhgr1v0e  29892  cplgrop  30075  finsumvtxdg2size  30188  rgrusgrprc  30227  elwspths2spth  30616  fusgr2wsp2nb  30992  h2hlm  31639  axhcompl-zf  31657  opsbc2ie  33171  inpr0  33226  iuninc  33253  disjpreima  33276  suppss2f  33330  fnpreimac  33362  tocyccntz  33804  elrgspnlem1  33902  elrgspnlem2  33903  nsgqusf1olem2  34069  nsgqusf1olem3  34070  cmpcref  34593  zarclsiin  34614  esumpfinvalf  34819  measiuns  34961  bnj23  35460  bnj110  35599  bnj1123  35727  bnj1373  35771  fineqvnttrclse  35933  kardeq0  35965  acycgr1v  36112  umgracycusgr  36117  cusgracyclt3v  36119  dmopab3rexdif  36378  wzel  36801  dfrdg4  36930  bj-sbeq  38028  bj-sbel1  38032  bj-snsetex  38091  bj-snglc  38097  bj-taginv  38114  bj-adjfrombun  38174  pibt2  38608  poimirlem16  38822  poimirlem19  38825  findcard4  38900  dfprop2  38914  eldmres  39475  ecres  39483  eldmqsres  39491  inxprnres  39496  cnvepres  39502  idinxpss  39516  inxpssidinxp  39520  idinxpssinxp  39521  cnvref5  39549  alrmomorn  39556  alrmomodm  39557  ssdmral  39577  brxrn  39581  dfxrn2  39583  dmcnvep  39586  inxpxrn  39616  rnxrn  39619  rnxrnres  39620  rnxrncnvepres  39621  rnxrnidres  39622  blockadjliftmap  39656  dfsucmap3  39661  dmsucmap  39666  dfsuccl4  39672  coss1cnvres  39705  coss2cnvepres  39706  1cossres  39717  dfcoels  39718  refressn  39731  br1cossinidres  39737  br1cossincnvepres  39738  br1cossxrnidres  39739  br1cossxrncnvepres  39740  refrelcosslem  39750  coss0  39767  cossid  39768  br1cossxrncnvssrres  39786  dfrefrels2  39791  dfcnvrefrels2  39806  dfcnvrefrels3  39807  dfsymrels2  39823  dftrrels2  39857  eldmqs1cossres  39942  disjimdmqseq  40007  dfeldisj5  40011  eldisjdmqsim  40015  disjres  40042  antisymrelres  40064  disjdmqsss  40103  disjdmqscossss  40104  mpets  40154  dmqsblocks  40165  dfpeters2  40172  prter2  40204  cdleme31sdnN  41710  evl1gprodd  43433  sn-iotalem  43542  inintabss  44840  inintabd  44841  cnvcnvintabd  44861  cnvintabd  44864  comptiunov2i  44967  cotrcltrcl  44986  corcltrcl  45000  cotrclrcl  45003  rr-grothprimbi  45540  rr-groth  45544  dfuniv2  45547  onfrALTlem4VD  46128  iinssiin  46417  iinssf  46426  iindif2f  46448  rnmptpr  46465  wessf1ornlem  46473  disjinfi  46480  rnmptlb  46528  rnmptbddlem  46529  rnmptbd2lem  46533  ellimcabssub0  46902  preimageiingt  48003  preimaleiinlt  48004  eusnsn  48369  dfdfat2  48471  iineq0  50262  iinxp  50273  mofeu  50290  tposres0  50321  iinfsubc  50503  onsetreclem1  51204