Theorem elv 3482

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  csbconstg  3926  csbvarg  4439  iinconst  5006  iuniin  5008  iinssiun  5009  iinss1  5011  ssiinf  5058  iinss  5060  iinss2  5061  iinab  5072  iinun2  5077  iundif2  5078  iindif1  5079  iindif2  5081  iinin2  5082  iinpw  5110  brab1  5195  triin  5281  eusvnf  5397  sbcop  5499  iunopab  5568  pwvabrel  5739  ssrel  5794  difopabOLD  5843  xpiindi  5848  dmopab2rex  5930  dfima2  6081  args  6112  inisegn0  6118  dffr3  6119  dfse2  6120  dfco2a  6267  dfpo2  6317  iotaval2  6530  iotavalOLD  6536  iinpreima  7088  tfinds2  7884  fvresex  7982  sbcoteq1a  8074  fnse  8156  xpord2pred  8168  xpord3lem  8172  xpord3pred  8175  suppvalbr  8187  cnvimadfsn  8195  reldmtpos  8257  rntpos  8262  ovtpos  8264  dftpos3  8267  tpostpos  8269  fprlem2  8324  wfrlem10OLD  8356  onovuni  8380  oarec  8598  eqerlem  8778  ixpiin  8962  ixpsnf1o  8976  boxriin  8978  idssen  9035  unxpdomlem3  9285  ac6sfi  9317  unbnn2  9330  fifo  9469  inf0  9658  ttrclselem2  9763  ttrclse  9764  rankxpsuc  9919  tcrank  9921  harcard  10015  infxpenlem  10050  infpwfien  10099  alephcard  10107  dfac3  10158  cflm  10287  fin23lem34  10383  dffin7-2  10435  fin1a2lem13  10449  itunitc1  10457  itunitc  10458  ituniiun  10459  hsmexlem4  10466  fin41  10481  axdclem2  10557  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  canthwe  10688  pwfseqlem5  10700  axgroth2  10862  axgroth6  10865  grothac  10867  grothtsk  10872  seqfeq4  14088  serle  14094  seqof  14096  hash1snb  14454  hashmap  14470  hashfun  14472  hashbclem  14487  hashf1lem2  14491  hashf1  14492  hash2prde  14505  prprrab  14508  hash3tpexb  14529  fi1uzind  14542  brfi1indALT  14545  s3sndisj  15002  s3iunsndisj  15003  rexfiuz  15382  fsumabs  15833  incexclem  15868  fprodcllemf  15990  fprodmodd  16029  iserodd  16868  hashbc0  17038  0ram  17053  ramub1  17061  initoid  18054  termoid  18055  equivestrcsetc  18207  gsumwspan  18871  gsmsymgrfix  19460  symgfixf1  19469  frgpnabllem1  19905  telgsums  20025  opprsubg  20368  subrngpropd  20584  subrgpropd  20624  coe1fzgsumdlem  22322  evl1gsumdlem  22375  mdetunilem9  22641  topnex  23018  neitr  23203  ordtbas2  23214  pnfnei  23243  mnfnei  23244  hauscmplem  23429  2ndcsb  23472  2ndcsep  23482  ptpjopn  23635  snfil  23887  fbasrn  23907  rnelfmlem  23975  rnelfm  23976  fmfnfmlem3  23979  fmfnfmlem4  23980  fmfnfm  23981  fclscmp  24053  alexsubALTlem4  24073  ptcmplem2  24076  symgtgp  24129  ustfilxp  24236  restutopopn  24262  ustuqtop2  24266  utopsnneiplem  24271  imasdsf1olem  24398  xpsdsval  24406  metuel2  24593  metustbl  24594  restmetu  24598  xrtgioo  24841  minveclem3b  25475  ovoliunlem1  25550  uniioombllem3  25633  itg1addlem4  25747  itg1addlem4OLD  25748  dvnff  25973  dvfsumlem3  26083  logfac  26657  gausslemma2dlem1a  27423  umgrislfupgrlem  29153  lfuhgr1v0e  29285  cplgrop  29468  finsumvtxdg2size  29582  rgrusgrprc  29621  elwspths2spth  29996  fusgr2wsp2nb  30362  h2hlm  31008  axhcompl-zf  31026  opsbc2ie  32503  inpr0  32557  iuninc  32580  disjpreima  32603  suppss2f  32654  fnpreimac  32687  tocyccntz  33146  elrgspnlem1  33231  elrgspnlem2  33232  nsgqusf1olem2  33421  nsgqusf1olem3  33422  zarclsiin  33831  esumpfinvalf  34056  measiuns  34197  bnj23  34710  bnj110  34850  bnj1123  34978  bnj1373  35022  lfuhgr2  35102  lfuhgr3  35103  acycgr1v  35133  umgracycusgr  35138  cusgracyclt3v  35140  dmopab3rexdif  35389  wzel  35805  dfrdg4  35932  bj-sbeq  36883  bj-sbel1  36887  bj-snsetex  36945  bj-snglc  36951  bj-taginv  36968  bj-adjfrombun  37028  poimirlem16  37622  poimirlem19  37625  eldmres  38251  ecres  38259  ecres2  38260  eldmqsres  38268  inxprnres  38273  cnvepres  38279  idinxpss  38293  inxpssidinxp  38297  idinxpssinxp  38298  cnvref5  38332  alrmomorn  38339  alrmomodm  38340  brxrn  38355  dfxrn2  38357  inxpxrn  38376  rnxrn  38379  rnxrnres  38380  rnxrncnvepres  38381  rnxrnidres  38382  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  38640  dfeldisj5  38702  disjres  38725  antisymrelres  38744  disjdmqsss  38783  disjdmqscossss  38784  mpets  38823  prter2  38862  cdleme31sdnN  40369  evl1gprodd  42098  sn-iotalem  42238  inintabss  43567  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  comptiunov2i  43695  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  rr-grothprimbi  44290  rr-groth  44294  dfuniv2  44297  onfrALTlem4VD  44883  iinssiin  45068  iinssf  45077  iindif2f  45102  rnmptpr  45119  wessf1ornlem  45127  disjinfi  45134  rnmptlb  45187  rnmptbddlem  45188  rnmptbd2lem  45192  ellimcabssub0  45572  eusnsn  46975  dfdfat2  47077  mofeu  48677  onsetreclem1  48935