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 ⊢ 𝜑

Syntax hints:   → wi 4   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456

This theorem is referenced by:  csbconstg  3871  csbvarg  4388  iinconst  4960  iuniin  4962  iinssiun  4963  iinss1  4965  ssiinf  5012  iinss  5014  iinss2  5015  iinab  5025  iinun2  5030  iundif2  5031  iindif1  5032  iindif2  5034  iinin2  5035  iinpw  5063  brab1  5148  triin  5224  eusvnf  5349  sbcop  5457  iunopab  5530  pwvabrel  5698  ssrel  5755  xpiindi  5807  cnv0  5855  dmopab2rex  5893  dfima2  6051  args  6081  inisegn0  6087  dffr3  6088  dfse2  6089  dfco2a  6233  dfpo2  6283  iotaval2  6492  iinpreima  7050  tfinds2  7844  fvresex  7941  sbcoteq1a  8032  fnse  8113  xpord2pred  8125  xpord3lem  8129  xpord3pred  8132  suppvalbr  8144  cnvimadfsn  8152  reldmtpos  8214  rntpos  8219  ovtpos  8221  dftpos3  8224  tpostpos  8226  fprlem2  8282  onovuni  8313  oarec  8531  eqerlem  8714  elecreseq  8728  ixpiin  8906  ixpsnf1o  8920  boxriin  8922  idssen  8978  unxpdomlem3  9202  ac6sfi  9228  unbnn2  9241  fifo  9378  inf0  9576  ttrclselem2  9681  ttrclse  9682  rankxpsuc  9840  tcrank  9842  harcard  9936  infxpenlem  9969  infpwfien  10018  alephcard  10026  dfac3  10077  cflm  10206  fin23lem34  10303  dffin7-2  10355  fin1a2lem13  10369  itunitc1  10377  itunitc  10378  ituniiun  10379  hsmexlem4  10386  fin41  10401  axdclem2  10477  fpwwe2lem11  10599  fpwwe2lem12  10600  fpwwe2  10601  canthwe  10609  pwfseqlem5  10621  axgroth2  10783  axgroth6  10786  grothac  10788  grothtsk  10793  seqfeq4  14064  serle  14070  seqof  14072  hash1snb  14432  hashmap  14448  hashfun  14450  hashbclem  14465  hashf1lem2  14469  hashf1  14470  hash2prde  14483  prprrab  14486  hash3tpexb  14507  fi1uzind  14520  brfi1indALT  14523  s3sndisj  14980  s3iunsndisj  14981  rexfiuz  15375  fsumabs  15829  incexclem  15866  fprodcllemf  15988  fprodmodd  16027  iserodd  16871  hashbc0  17041  0ram  17056  ramub1  17064  initoid  18034  termoid  18035  equivestrcsetc  18184  gsumwspan  18880  gsmsymgrfix  19468  symgfixf1  19477  frgpnabllem1  19913  telgsums  20033  opprsubg  20401  subrngpropd  20618  subrgpropd  20658  coe1fzgsumdlem  22366  evl1gsumdlem  22419  mdetunilem9  22680  topnex  23056  neitr  23240  ordtbas2  23251  pnfnei  23280  mnfnei  23281  hauscmplem  23466  2ndcsb  23509  2ndcsep  23519  ptpjopn  23672  snfil  23924  fbasrn  23944  rnelfmlem  24012  rnelfm  24013  fmfnfmlem3  24016  fmfnfmlem4  24017  fmfnfm  24018  fclscmp  24090  alexsubALTlem4  24110  ptcmplem2  24113  symgtgp  24166  ustfilxp  24273  restutopopn  24298  ustuqtop2  24302  utopsnneiplem  24307  imasdsf1olem  24433  xpsdsval  24441  metuel2  24625  metustbl  24626  restmetu  24630  xrtgioo  24867  minveclem3b  25490  ovoliunlem1  25564  uniioombllem3  25647  itg1addlem4  25761  dvnff  25985  dvfsumlem3  26090  logfac  26666  gausslemma2dlem1a  27429  onsis  28367  ons2ind  28368  umgrislfupgrlem  29323  lfuhgr1v0e  29455  cplgrop  29638  finsumvtxdg2size  29751  rgrusgrprc  29790  elwspths2spth  30170  fusgr2wsp2nb  30536  h2hlm  31183  axhcompl-zf  31201  opsbc2ie  32675  inpr0  32731  iuninc  32760  disjpreima  32784  suppss2f  32840  fnpreimac  32872  tocyccntz  33324  elrgspnlem1  33423  elrgspnlem2  33424  nsgqusf1olem2  33600  nsgqusf1olem3  33601  zarclsiin  34168  esumpfinvalf  34373  measiuns  34514  bnj23  35014  bnj110  35153  bnj1123  35281  bnj1373  35325  fineqvnttrclse  35420  lfuhgr2  35469  lfuhgr3  35470  acycgr1v  35499  umgracycusgr  35504  cusgracyclt3v  35506  dmopab3rexdif  35755  wzel  36172  dfrdg4  36301  bj-sbeq  37386  bj-sbel1  37390  bj-snsetex  37448  bj-snglc  37454  bj-taginv  37471  bj-adjfrombun  37531  poimirlem16  38135  poimirlem19  38138  eldmres  38776  ecres  38784  eldmqsres  38792  inxprnres  38797  cnvepres  38803  idinxpss  38817  inxpssidinxp  38821  idinxpssinxp  38822  cnvref5  38850  alrmomorn  38857  alrmomodm  38858  ssdmral  38878  brxrn  38882  dfxrn2  38884  dmcnvep  38887  inxpxrn  38917  rnxrn  38920  rnxrnres  38921  rnxrncnvepres  38922  rnxrnidres  38923  blockadjliftmap  38957  dfsucmap3  38962  dmsucmap  38967  dfsuccl4  38973  coss1cnvres  39006  coss2cnvepres  39007  1cossres  39018  dfcoels  39019  refressn  39032  br1cossinidres  39038  br1cossincnvepres  39039  br1cossxrnidres  39040  br1cossxrncnvepres  39041  refrelcosslem  39051  coss0  39068  cossid  39069  br1cossxrncnvssrres  39087  dfrefrels2  39092  dfcnvrefrels2  39107  dfcnvrefrels3  39108  dfsymrels2  39124  dftrrels2  39158  eldmqs1cossres  39243  disjimdmqseq  39308  dfeldisj5  39312  eldisjdmqsim  39316  disjres  39343  antisymrelres  39365  disjdmqsss  39404  disjdmqscossss  39405  mpets  39455  dmqsblocks  39466  dfpeters2  39473  prter2  39505  cdleme31sdnN  41011  evl1gprodd  42734  sn-iotalem  42840  inintabss  44154  inintabd  44155  cnvcnvintabd  44176  cnvintabd  44179  comptiunov2i  44282  cotrcltrcl  44301  corcltrcl  44315  cotrclrcl  44318  rr-grothprimbi  44871  rr-groth  44875  dfuniv2  44878  onfrALTlem4VD  45461  iinssiin  45707  iinssf  45716  iindif2f  45738  rnmptpr  45755  wessf1ornlem  45763  disjinfi  45770  rnmptlb  45818  rnmptbddlem  45819  rnmptbd2lem  45823  ellimcabssub0  46193  preimageiingt  47294  preimaleiinlt  47295  eusnsn  47620  dfdfat2  47722  iineq0  49441  iinxp  49452  mofeu  49469  tposres0  49498  iinfsubc  49679  onsetreclem1  50326