Theorem elv 3441

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438

This theorem is referenced by:  csbconstg  3870  csbvarg  4385  iinconst  4952  iuniin  4954  iinssiun  4955  iinss1  4957  ssiinf  5003  iinss  5005  iinss2  5006  iinab  5017  iinun2  5022  iundif2  5023  iindif1  5024  iindif2  5026  iinin2  5027  iinpw  5055  brab1  5140  triin  5215  eusvnf  5331  sbcop  5432  iunopab  5502  pwvabrel  5670  ssrel  5726  xpiindi  5778  dmopab2rex  5860  dfima2  6013  args  6043  inisegn0  6049  dffr3  6050  dfse2  6051  dfco2a  6195  dfpo2  6244  iotaval2  6453  iinpreima  7003  tfinds2  7797  fvresex  7895  sbcoteq1a  7986  fnse  8066  xpord2pred  8078  xpord3lem  8082  xpord3pred  8085  suppvalbr  8097  cnvimadfsn  8105  reldmtpos  8167  rntpos  8172  ovtpos  8174  dftpos3  8177  tpostpos  8179  fprlem2  8234  onovuni  8265  oarec  8480  eqerlem  8660  elecreseq  8674  ixpiin  8851  ixpsnf1o  8865  boxriin  8867  idssen  8922  unxpdomlem3  9147  ac6sfi  9173  unbnn2  9186  fifo  9322  inf0  9517  ttrclselem2  9622  ttrclse  9623  rankxpsuc  9778  tcrank  9780  harcard  9874  infxpenlem  9907  infpwfien  9956  alephcard  9964  dfac3  10015  cflm  10144  fin23lem34  10240  dffin7-2  10292  fin1a2lem13  10306  itunitc1  10314  itunitc  10315  ituniiun  10316  hsmexlem4  10323  fin41  10338  axdclem2  10414  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  canthwe  10545  pwfseqlem5  10557  axgroth2  10719  axgroth6  10722  grothac  10724  grothtsk  10729  seqfeq4  13958  serle  13964  seqof  13966  hash1snb  14326  hashmap  14342  hashfun  14344  hashbclem  14359  hashf1lem2  14363  hashf1  14364  hash2prde  14377  prprrab  14380  hash3tpexb  14401  fi1uzind  14414  brfi1indALT  14417  s3sndisj  14874  s3iunsndisj  14875  rexfiuz  15255  fsumabs  15708  incexclem  15743  fprodcllemf  15865  fprodmodd  15904  iserodd  16747  hashbc0  16917  0ram  16932  ramub1  16940  initoid  17908  termoid  17909  equivestrcsetc  18058  gsumwspan  18720  gsmsymgrfix  19307  symgfixf1  19316  frgpnabllem1  19752  telgsums  19872  opprsubg  20237  subrngpropd  20453  subrgpropd  20493  coe1fzgsumdlem  22188  evl1gsumdlem  22241  mdetunilem9  22505  topnex  22881  neitr  23065  ordtbas2  23076  pnfnei  23105  mnfnei  23106  hauscmplem  23291  2ndcsb  23334  2ndcsep  23344  ptpjopn  23497  snfil  23749  fbasrn  23769  rnelfmlem  23837  rnelfm  23838  fmfnfmlem3  23841  fmfnfmlem4  23842  fmfnfm  23843  fclscmp  23915  alexsubALTlem4  23935  ptcmplem2  23938  symgtgp  23991  ustfilxp  24098  restutopopn  24124  ustuqtop2  24128  utopsnneiplem  24133  imasdsf1olem  24259  xpsdsval  24267  metuel2  24451  metustbl  24452  restmetu  24456  xrtgioo  24693  minveclem3b  25326  ovoliunlem1  25401  uniioombllem3  25484  itg1addlem4  25598  dvnff  25823  dvfsumlem3  25933  logfac  26508  gausslemma2dlem1a  27274  onsis  28177  umgrislfupgrlem  29067  lfuhgr1v0e  29199  cplgrop  29382  finsumvtxdg2size  29496  rgrusgrprc  29535  elwspths2spth  29912  fusgr2wsp2nb  30278  h2hlm  30924  axhcompl-zf  30942  opsbc2ie  32420  inpr0  32476  iuninc  32504  disjpreima  32528  suppss2f  32581  fnpreimac  32614  tocyccntz  33086  elrgspnlem1  33182  elrgspnlem2  33183  nsgqusf1olem2  33351  nsgqusf1olem3  33352  zarclsiin  33838  esumpfinvalf  34043  measiuns  34184  bnj23  34685  bnj110  34825  bnj1123  34953  bnj1373  34997  fineqvnttrclse  35077  lfuhgr2  35096  lfuhgr3  35097  acycgr1v  35126  umgracycusgr  35131  cusgracyclt3v  35133  dmopab3rexdif  35382  wzel  35802  dfrdg4  35929  bj-sbeq  36879  bj-sbel1  36883  bj-snsetex  36941  bj-snglc  36947  bj-taginv  36964  bj-adjfrombun  37024  poimirlem16  37620  poimirlem19  37623  eldmres  38249  ecres  38257  eldmqsres  38265  inxprnres  38270  cnvepres  38276  idinxpss  38290  inxpssidinxp  38294  idinxpssinxp  38295  cnvref5  38323  alrmomorn  38330  alrmomodm  38331  brxrn  38346  dfxrn2  38348  dmcnvep  38351  inxpxrn  38371  rnxrn  38374  rnxrnres  38375  rnxrncnvepres  38376  rnxrnidres  38377  coss1cnvres  38398  coss2cnvepres  38399  1cossres  38410  dfcoels  38411  refressn  38424  br1cossinidres  38430  br1cossincnvepres  38431  br1cossxrnidres  38432  br1cossxrncnvepres  38433  refrelcosslem  38443  coss0  38460  cossid  38461  br1cossxrncnvssrres  38489  dfrefrels2  38494  dfcnvrefrels2  38509  dfcnvrefrels3  38510  dfsymrels2  38526  dftrrels2  38556  eldmqs1cossres  38641  dfeldisj5  38703  disjres  38726  antisymrelres  38745  disjdmqsss  38784  disjdmqscossss  38785  mpets  38824  dmqsblocks  38835  prter2  38864  cdleme31sdnN  40370  evl1gprodd  42094  sn-iotalem  42198  inintabss  43555  inintabd  43556  cnvcnvintabd  43577  cnvintabd  43580  comptiunov2i  43683  cotrcltrcl  43702  corcltrcl  43716  cotrclrcl  43719  rr-grothprimbi  44272  rr-groth  44276  dfuniv2  44279  onfrALTlem4VD  44863  iinssiin  45111  iinssf  45120  iindif2f  45142  rnmptpr  45159  wessf1ornlem  45167  disjinfi  45174  rnmptlb  45225  rnmptbddlem  45226  rnmptbd2lem  45230  ellimcabssub0  45602  eusnsn  47014  dfdfat2  47116  iineq0  48808  iinxp  48819  mofeu  48836  tposres0  48865  iinfsubc  49047  onsetreclem1  49694