Theorem elv 3472

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468

This theorem is referenced by:  csbconstg  3904  csbvarg  4423  iinconst  4997  iuniin  4999  iinssiun  5000  iinss1  5002  ssiinf  5047  iinss  5049  iinss2  5050  iinab  5061  iinun2  5066  iundif2  5067  iindif1  5068  iindif2  5070  iinin2  5071  iinpw  5099  brab1  5186  triin  5272  eusvnf  5380  sbcop  5479  iunopab  5549  pwvabrel  5717  ssrel  5772  difopabOLD  5821  xpiindi  5825  dmopab2rex  5907  dfima2  6051  args  6081  inisegn0  6087  dffr3  6088  dfse2  6089  dfco2a  6235  dfpo2  6285  iotaval2  6501  iotavalOLD  6507  iinpreima  7060  tfinds2  7846  fvresex  7939  sbcoteq1a  8030  fnse  8113  xpord2pred  8125  xpord3lem  8129  xpord3pred  8132  suppvalbr  8144  cnvimadfsn  8151  reldmtpos  8214  rntpos  8219  ovtpos  8221  dftpos3  8224  tpostpos  8226  fprlem2  8281  wfrlem10OLD  8313  onovuni  8337  oarec  8557  eqerlem  8733  ixpiin  8914  ixpsnf1o  8928  boxriin  8930  idssen  8989  unxpdomlem3  9248  ac6sfi  9283  unbnn2  9296  fifo  9423  inf0  9612  ttrclselem2  9717  ttrclse  9718  rankxpsuc  9873  tcrank  9875  harcard  9969  infxpenlem  10004  infpwfien  10053  alephcard  10061  dfac3  10112  cflm  10241  fin23lem34  10337  dffin7-2  10389  fin1a2lem13  10403  itunitc1  10411  itunitc  10412  ituniiun  10413  hsmexlem4  10420  fin41  10435  axdclem2  10511  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  canthwe  10642  pwfseqlem5  10654  axgroth2  10816  axgroth6  10819  grothac  10821  grothtsk  10826  seqfeq4  14014  serle  14020  seqof  14022  hash1snb  14376  hashmap  14392  hashfun  14394  hashbclem  14408  hashf1lem2  14414  hashf1  14415  hash2prde  14428  prprrab  14431  fi1uzind  14455  brfi1indALT  14458  s3sndisj  14911  s3iunsndisj  14912  rexfiuz  15291  fsumabs  15744  incexclem  15779  fprodcllemf  15899  fprodmodd  15938  iserodd  16767  hashbc0  16937  0ram  16952  ramub1  16960  initoid  17953  termoid  17954  equivestrcsetc  18106  gsumwspan  18761  gsmsymgrfix  19338  symgfixf1  19347  frgpnabllem1  19783  telgsums  19903  opprsubg  20244  subrngpropd  20458  subrgpropd  20500  coe1fzgsumdlem  22144  evl1gsumdlem  22197  mdetunilem9  22444  topnex  22821  neitr  23006  ordtbas2  23017  pnfnei  23046  mnfnei  23047  hauscmplem  23232  2ndcsb  23275  2ndcsep  23285  ptpjopn  23438  snfil  23690  fbasrn  23710  rnelfmlem  23778  rnelfm  23779  fmfnfmlem3  23782  fmfnfmlem4  23783  fmfnfm  23784  fclscmp  23856  alexsubALTlem4  23876  ptcmplem2  23879  symgtgp  23932  ustfilxp  24039  restutopopn  24065  ustuqtop2  24069  utopsnneiplem  24074  imasdsf1olem  24201  xpsdsval  24209  metuel2  24396  metustbl  24397  restmetu  24401  xrtgioo  24644  minveclem3b  25278  ovoliunlem1  25353  uniioombllem3  25436  itg1addlem4  25550  itg1addlem4OLD  25551  dvnff  25775  dvfsumlem3  25885  logfac  26451  gausslemma2dlem1a  27214  umgrislfupgrlem  28851  lfuhgr1v0e  28980  cplgrop  29163  finsumvtxdg2size  29276  rgrusgrprc  29315  elwspths2spth  29690  fusgr2wsp2nb  30056  h2hlm  30702  axhcompl-zf  30720  opsbc2ie  32185  inpr0  32238  iuninc  32261  disjpreima  32284  suppss2f  32332  fnpreimac  32365  tocyccntz  32771  nsgqusf1olem2  32994  nsgqusf1olem3  32995  zarclsiin  33340  esumpfinvalf  33563  measiuns  33704  bnj23  34218  bnj110  34358  bnj1123  34486  bnj1373  34530  lfuhgr2  34598  lfuhgr3  34599  acycgr1v  34629  umgracycusgr  34634  cusgracyclt3v  34636  dmopab3rexdif  34885  wzel  35291  dfrdg4  35418  bj-sbeq  36271  bj-sbel1  36275  bj-snsetex  36334  bj-snglc  36340  bj-taginv  36357  bj-adjfrombun  36417  poimirlem16  36994  poimirlem19  36997  eldmres  37628  ecres  37636  ecres2  37637  eldmqsres  37645  inxprnres  37651  cnvepres  37657  idinxpss  37671  inxpssidinxp  37675  idinxpssinxp  37676  cnvref5  37710  alrmomorn  37717  alrmomodm  37718  brxrn  37734  dfxrn2  37736  inxpxrn  37755  rnxrn  37758  rnxrnres  37759  rnxrncnvepres  37760  rnxrnidres  37761  coss1cnvres  37777  coss2cnvepres  37778  1cossres  37789  dfcoels  37790  refressn  37803  br1cossinidres  37809  br1cossincnvepres  37810  br1cossxrnidres  37811  br1cossxrncnvepres  37812  refrelcosslem  37822  coss0  37839  cossid  37840  br1cossxrncnvssrres  37868  dfrefrels2  37873  dfcnvrefrels2  37888  dfcnvrefrels3  37889  dfsymrels2  37905  dftrrels2  37935  eldmqs1cossres  38019  dfeldisj5  38081  disjres  38104  antisymrelres  38123  disjdmqsss  38162  disjdmqscossss  38163  mpets  38202  prter2  38241  cdleme31sdnN  39748  sn-iotalem  41531  inintabss  42818  inintabd  42819  cnvcnvintabd  42840  cnvintabd  42843  comptiunov2i  42946  cotrcltrcl  42965  corcltrcl  42979  cotrclrcl  42982  rr-grothprimbi  43543  rr-groth  43547  dfuniv2  43550  onfrALTlem4VD  44136  iinssiin  44306  iinssf  44315  iindif2f  44342  rnmptpr  44361  wessf1ornlem  44369  disjinfi  44376  rnmptlb  44432  rnmptbddlem  44433  rnmptbd2lem  44437  ellimcabssub0  44818  eusnsn  46221  dfdfat2  46321  mofeu  47702  onsetreclem1  47938