Theorem elv 3493

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  csbconstg  3940  csbvarg  4457  iinconst  5025  iuniin  5027  iinssiun  5028  iinss1  5030  ssiinf  5077  iinss  5079  iinss2  5080  iinab  5091  iinun2  5096  iundif2  5097  iindif1  5098  iindif2  5100  iinin2  5101  iinpw  5129  brab1  5214  triin  5300  eusvnf  5410  sbcop  5509  iunopab  5578  pwvabrel  5751  ssrel  5806  difopabOLD  5855  xpiindi  5860  dmopab2rex  5942  dfima2  6091  args  6122  inisegn0  6128  dffr3  6129  dfse2  6130  dfco2a  6277  dfpo2  6327  iotaval2  6541  iotavalOLD  6547  iinpreima  7102  tfinds2  7901  fvresex  8000  sbcoteq1a  8092  fnse  8174  xpord2pred  8186  xpord3lem  8190  xpord3pred  8193  suppvalbr  8205  cnvimadfsn  8213  reldmtpos  8275  rntpos  8280  ovtpos  8282  dftpos3  8285  tpostpos  8287  fprlem2  8342  wfrlem10OLD  8374  onovuni  8398  oarec  8618  eqerlem  8798  ixpiin  8982  ixpsnf1o  8996  boxriin  8998  idssen  9057  unxpdomlem3  9315  ac6sfi  9348  unbnn2  9361  fifo  9501  inf0  9690  ttrclselem2  9795  ttrclse  9796  rankxpsuc  9951  tcrank  9953  harcard  10047  infxpenlem  10082  infpwfien  10131  alephcard  10139  dfac3  10190  cflm  10319  fin23lem34  10415  dffin7-2  10467  fin1a2lem13  10481  itunitc1  10489  itunitc  10490  ituniiun  10491  hsmexlem4  10498  fin41  10513  axdclem2  10589  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  canthwe  10720  pwfseqlem5  10732  axgroth2  10894  axgroth6  10897  grothac  10899  grothtsk  10904  seqfeq4  14102  serle  14108  seqof  14110  hash1snb  14468  hashmap  14484  hashfun  14486  hashbclem  14501  hashf1lem2  14505  hashf1  14506  hash2prde  14519  prprrab  14522  hash3tpexb  14543  fi1uzind  14556  brfi1indALT  14559  s3sndisj  15016  s3iunsndisj  15017  rexfiuz  15396  fsumabs  15849  incexclem  15884  fprodcllemf  16006  fprodmodd  16045  iserodd  16882  hashbc0  17052  0ram  17067  ramub1  17075  initoid  18068  termoid  18069  equivestrcsetc  18221  gsumwspan  18881  gsmsymgrfix  19470  symgfixf1  19479  frgpnabllem1  19915  telgsums  20035  opprsubg  20378  subrngpropd  20594  subrgpropd  20636  coe1fzgsumdlem  22328  evl1gsumdlem  22381  mdetunilem9  22647  topnex  23024  neitr  23209  ordtbas2  23220  pnfnei  23249  mnfnei  23250  hauscmplem  23435  2ndcsb  23478  2ndcsep  23488  ptpjopn  23641  snfil  23893  fbasrn  23913  rnelfmlem  23981  rnelfm  23982  fmfnfmlem3  23985  fmfnfmlem4  23986  fmfnfm  23987  fclscmp  24059  alexsubALTlem4  24079  ptcmplem2  24082  symgtgp  24135  ustfilxp  24242  restutopopn  24268  ustuqtop2  24272  utopsnneiplem  24277  imasdsf1olem  24404  xpsdsval  24412  metuel2  24599  metustbl  24600  restmetu  24604  xrtgioo  24847  minveclem3b  25481  ovoliunlem1  25556  uniioombllem3  25639  itg1addlem4  25753  itg1addlem4OLD  25754  dvnff  25979  dvfsumlem3  26089  logfac  26661  gausslemma2dlem1a  27427  umgrislfupgrlem  29157  lfuhgr1v0e  29289  cplgrop  29472  finsumvtxdg2size  29586  rgrusgrprc  29625  elwspths2spth  30000  fusgr2wsp2nb  30366  h2hlm  31012  axhcompl-zf  31030  opsbc2ie  32504  inpr0  32560  iuninc  32583  disjpreima  32606  suppss2f  32657  fnpreimac  32689  tocyccntz  33137  nsgqusf1olem2  33407  nsgqusf1olem3  33408  zarclsiin  33817  esumpfinvalf  34040  measiuns  34181  bnj23  34694  bnj110  34834  bnj1123  34962  bnj1373  35006  lfuhgr2  35086  lfuhgr3  35087  acycgr1v  35117  umgracycusgr  35122  cusgracyclt3v  35124  dmopab3rexdif  35373  wzel  35788  dfrdg4  35915  bj-sbeq  36867  bj-sbel1  36871  bj-snsetex  36929  bj-snglc  36935  bj-taginv  36952  bj-adjfrombun  37012  poimirlem16  37596  poimirlem19  37599  eldmres  38226  ecres  38234  ecres2  38235  eldmqsres  38243  inxprnres  38248  cnvepres  38254  idinxpss  38268  inxpssidinxp  38272  idinxpssinxp  38273  cnvref5  38307  alrmomorn  38314  alrmomodm  38315  brxrn  38330  dfxrn2  38332  inxpxrn  38351  rnxrn  38354  rnxrnres  38355  rnxrncnvepres  38356  rnxrnidres  38357  coss1cnvres  38373  coss2cnvepres  38374  1cossres  38385  dfcoels  38386  refressn  38399  br1cossinidres  38405  br1cossincnvepres  38406  br1cossxrnidres  38407  br1cossxrncnvepres  38408  refrelcosslem  38418  coss0  38435  cossid  38436  br1cossxrncnvssrres  38464  dfrefrels2  38469  dfcnvrefrels2  38484  dfcnvrefrels3  38485  dfsymrels2  38501  dftrrels2  38531  eldmqs1cossres  38615  dfeldisj5  38677  disjres  38700  antisymrelres  38719  disjdmqsss  38758  disjdmqscossss  38759  mpets  38798  prter2  38837  cdleme31sdnN  40344  evl1gprodd  42074  sn-iotalem  42214  inintabss  43540  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  comptiunov2i  43668  cotrcltrcl  43687  corcltrcl  43701  cotrclrcl  43704  rr-grothprimbi  44264  rr-groth  44268  dfuniv2  44271  onfrALTlem4VD  44857  iinssiin  45031  iinssf  45040  iindif2f  45065  rnmptpr  45084  wessf1ornlem  45092  disjinfi  45099  rnmptlb  45152  rnmptbddlem  45153  rnmptbd2lem  45157  ellimcabssub0  45538  eusnsn  46941  dfdfat2  47043  mofeu  48561  onsetreclem1  48797