Theorem elv 3458

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455

This theorem is used by:  csbconstg  3869  csbvarg  4394  iinconst  4964  iuniin  4966  iinssiun  4967  iinss1  4969  ssiinf  5015  iinss  5017  iinss2  5018  iinab  5028  iinun2  5033  iundif2  5034  iindif1  5037  iindif2  5039  iinin2  5040  iinpw  5068  brab1  5155  triin  5231  eusvnf  5357  sbcop  5462  iunopab  5537  pwvabrel  5705  ssrel  5763  xpiindi  5816  cnv0  5865  dmopab2rex  5903  dfima2  6063  args  6095  inisegn0  6101  dffr3  6102  dfse2  6103  dfco2a  6253  dfpo2  6305  iotaval2  6515  iinpreima  7077  tfinds2  7882  fvresex  7979  sbcoteq1a  8070  fnse  8160  xpord2pred  8172  xpord3lem  8176  xpord3pred  8179  suppvalbr  8191  suppvalbrOLD  8192  cnvimadfsn  8200  reldmtpos  8262  rntpos  8267  ovtpos  8269  dftpos3  8272  tpostpos  8274  fprlem2  8330  onovuni  8361  oarec  8581  eqerlem  8764  elecreseq  8778  ixpiin  8963  ixpsnf1o  8977  boxriin  8979  idssen  9035  unxpdomlem3  9260  ac6sfi  9286  unbnn2  9300  fifo  9434  inf0  9632  ttrclselem2  9737  ttrclse  9738  rankxpsuc  9909  tcrank  9911  harcard  10069  infxpenlem  10102  infpwfien  10151  alephcard  10159  dfac3  10210  cflm  10337  fin23lem34  10434  dffin7-2  10486  fin1a2lem13  10500  itunitc1  10508  itunitc  10509  ituniiun  10510  hsmexlem4  10517  fin41  10532  axdclem2  10608  fpwwe2lem11  10736  fpwwe2lem12  10737  fpwwe2  10738  canthwe  10746  pwfseqlem5  10758  axgroth2  10920  axgroth6  10923  grothac  10925  grothtsk  10930  seqfeq4  14204  serle  14210  seqof  14212  hash1snb  14574  hashmap  14590  hashfun  14592  hashbclem  14607  hashf1lem2  14611  hashf1  14612  hash2prde  14625  prprrab  14628  hash3tpexb  14649  fi1uzind  14662  brfi1indALT  14665  s3sndisj  15132  s3iunsndisj  15133  rexfiuz  15527  fsumabs  15980  incexclem  16017  fprodcllemf  16137  fprodmodd  16176  iserodd  17025  hashbc0  17195  0ram  17210  ramub1  17218  initoid  18188  termoid  18189  equivestrcsetc  18338  gsumwspan  19054  gsmsymgrfix  19654  symgfixf1  19663  frgpnabllem1  20099  telgsums  20219  opprsubg  20594  subrngpropd  20832  subrgpropd  20872  coe1fzgsumdlem  22633  evl1gsumdlem  22686  mdetunilem9  22947  topnex  23326  neitr  23510  ordtbas2  23521  pnfnei  23550  mnfnei  23551  hauscmplem  23736  2ndcsb  23779  2ndcsep  23790  ptpjopn  23943  snfil  24195  fbasrn  24215  rnelfmlem  24283  rnelfm  24284  fmfnfmlem3  24287  fmfnfmlem4  24288  fmfnfm  24289  fclscmp  24361  alexsubALTlem4  24381  ptcmplem2  24384  symgtgp  24437  ustfilxp  24544  restutopopn  24569  ustuqtop2  24573  utopsnneiplem  24578  imasdsf1olem  24704  xpsdsval  24712  metuel2  24896  metustbl  24897  restmetu  24901  xrtgioo  25138  minveclem3b  25761  ovoliunlem1  25835  uniioombllem3  25918  itg1addlem4  26032  dvnff  26255  dvfsumlem3  26360  logfac  26941  gausslemma2dlem1a  27704  onsis  28672  ons2ind  28673  umgrislfupgrlem  29712  lfuhgr2  29739  lfuhgr3  29740  lfuhgr1v0e  29847  cplgrop  30030  finsumvtxdg2size  30143  rgrusgrprc  30182  elwspths2spth  30571  fusgr2wsp2nb  30947  h2hlm  31594  axhcompl-zf  31612  opsbc2ie  33126  inpr0  33182  iuninc  33209  disjpreima  33232  suppss2f  33286  fnpreimac  33318  tocyccntz  33758  elrgspnlem1  33856  elrgspnlem2  33857  nsgqusf1olem2  34018  nsgqusf1olem3  34019  cmpcref  34535  zarclsiin  34556  esumpfinvalf  34761  measiuns  34903  bnj23  35402  bnj110  35541  bnj1123  35669  bnj1373  35713  fineqvnttrclse  35863  kardeq0  35895  acycgr1v  36025  umgracycusgr  36030  cusgracyclt3v  36032  dmopab3rexdif  36291  wzel  36713  dfrdg4  36842  bj-sbeq  37940  bj-sbel1  37944  bj-snsetex  38003  bj-snglc  38009  bj-taginv  38026  bj-adjfrombun  38086  pibt2  38480  poimirlem16  38694  poimirlem19  38697  findcard4  38772  dfprop2  38786  eldmres  39349  ecres  39357  eldmqsres  39365  inxprnres  39370  cnvepres  39376  idinxpss  39390  inxpssidinxp  39394  idinxpssinxp  39395  cnvref5  39423  alrmomorn  39430  alrmomodm  39431  ssdmral  39451  brxrn  39455  dfxrn2  39457  dmcnvep  39460  inxpxrn  39490  rnxrn  39493  rnxrnres  39494  rnxrncnvepres  39495  rnxrnidres  39496  blockadjliftmap  39530  dfsucmap3  39535  dmsucmap  39540  dfsuccl4  39546  coss1cnvres  39579  coss2cnvepres  39580  1cossres  39591  dfcoels  39592  refressn  39605  br1cossinidres  39611  br1cossincnvepres  39612  br1cossxrnidres  39613  br1cossxrncnvepres  39614  refrelcosslem  39624  coss0  39641  cossid  39642  br1cossxrncnvssrres  39660  dfrefrels2  39665  dfcnvrefrels2  39680  dfcnvrefrels3  39681  dfsymrels2  39697  dftrrels2  39731  eldmqs1cossres  39816  disjimdmqseq  39881  dfeldisj5  39885  eldisjdmqsim  39889  disjres  39916  antisymrelres  39938  disjdmqsss  39977  disjdmqscossss  39978  mpets  40028  dmqsblocks  40039  dfpeters2  40046  prter2  40078  cdleme31sdnN  41584  evl1gprodd  43307  sn-iotalem  43415  inintabss  44719  inintabd  44720  cnvcnvintabd  44740  cnvintabd  44743  comptiunov2i  44846  cotrcltrcl  44865  corcltrcl  44879  cotrclrcl  44882  rr-grothprimbi  45419  rr-groth  45423  dfuniv2  45426  onfrALTlem4VD  46007  iinssiin  46283  iinssf  46292  iindif2f  46314  rnmptpr  46331  wessf1ornlem  46339  disjinfi  46346  rnmptlb  46394  rnmptbddlem  46395  rnmptbd2lem  46399  ellimcabssub0  46768  preimageiingt  47869  preimaleiinlt  47870  eusnsn  48235  dfdfat2  48337  iineq0  50070  iinxp  50081  mofeu  50098  tposres0  50129  iinfsubc  50311  onsetreclem1  51012