Theorem elv 3439

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  csbconstg  3852  csbvarg  4366  dfopif  4801  iinconst  4935  iuniin  4937  iinssiun  4938  iinss1  4940  ssiinf  4985  iinss  4987  iinss2  4988  iinab  4998  iinun2  5003  iundif2  5004  iindif1  5005  iindif2  5007  iinin2  5008  iinpw  5036  brab1  5123  triin  5207  eusvnf  5316  sbcop  5404  iunopab  5473  pwvabrel  5639  ssrel  5694  difopabOLD  5743  xpiindi  5747  dmopab2rex  5829  dfima2  5974  args  6003  inisegn0  6009  dffr3  6010  dfse2  6011  dfco2a  6154  dfpo2  6203  iotaval  6411  iinpreima  6955  tfinds2  7719  fvresex  7811  fnse  7983  suppvalbr  7990  cnvimadfsn  7997  reldmtpos  8059  rntpos  8064  ovtpos  8066  dftpos3  8069  tpostpos  8071  fprlem2  8126  wfrlem10OLD  8158  onovuni  8182  oarec  8402  eqerlem  8541  ixpiin  8721  ixpsnf1o  8735  boxriin  8737  idssen  8794  unxpdomlem3  9038  ac6sfi  9067  unbnn2  9080  fifo  9200  inf0  9388  ttrclselem2  9493  ttrclse  9494  rankxpsuc  9649  tcrank  9651  harcard  9745  infxpenlem  9778  infpwfien  9827  alephcard  9835  dfac3  9886  cflm  10015  fin23lem34  10111  dffin7-2  10163  fin1a2lem13  10177  itunitc1  10185  itunitc  10186  ituniiun  10187  hsmexlem4  10194  fin41  10209  axdclem2  10285  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  canthwe  10416  pwfseqlem5  10428  axgroth2  10590  axgroth6  10593  grothac  10595  grothtsk  10600  seqfeq4  13781  serle  13787  seqof  13789  hash1snb  14143  hashmap  14159  hashfun  14161  hashbclem  14173  hashf1lem2  14179  hashf1  14180  hash2prde  14193  prprrab  14196  fi1uzind  14220  brfi1indALT  14223  s3sndisj  14687  s3iunsndisj  14688  rexfiuz  15068  fsumabs  15522  incexclem  15557  fprodcllemf  15677  fprodmodd  15716  iserodd  16545  hashbc0  16715  0ram  16730  ramub1  16738  initoid  17725  termoid  17726  equivestrcsetc  17878  gsumwspan  18494  gsmsymgrfix  19045  symgfixf1  19054  frgpnabllem1  19483  telgsums  19603  opprsubg  19887  subrgpropd  20068  coe1fzgsumdlem  21481  evl1gsumdlem  21531  mdetunilem9  21778  topnex  22155  neitr  22340  ordtbas2  22351  pnfnei  22380  mnfnei  22381  hauscmplem  22566  2ndcsb  22609  2ndcsep  22619  ptpjopn  22772  snfil  23024  fbasrn  23044  rnelfmlem  23112  rnelfm  23113  fmfnfmlem3  23116  fmfnfmlem4  23117  fmfnfm  23118  fclscmp  23190  alexsubALTlem4  23210  ptcmplem2  23213  symgtgp  23266  ustfilxp  23373  restutopopn  23399  ustuqtop2  23403  utopsnneiplem  23408  imasdsf1olem  23535  xpsdsval  23543  metuel2  23730  metustbl  23731  restmetu  23735  xrtgioo  23978  minveclem3b  24601  ovoliunlem1  24675  uniioombllem3  24758  itg1addlem4  24872  itg1addlem4OLD  24873  dvnff  25096  dvfsumlem3  25201  logfac  25765  gausslemma2dlem1a  26522  umgrislfupgrlem  27501  lfuhgr1v0e  27630  cplgrop  27813  finsumvtxdg2size  27926  rgrusgrprc  27965  elwspths2spth  28341  fusgr2wsp2nb  28707  h2hlm  29351  axhcompl-zf  29369  opsbc2ie  30833  inpr0  30889  iuninc  30909  disjpreima  30932  suppss2f  30983  fnpreimac  31017  tocyccntz  31420  nsgqusf1olem2  31608  nsgqusf1olem3  31609  zarclsiin  31830  esumpfinvalf  32053  measiuns  32194  bnj23  32706  bnj110  32847  bnj1123  32975  bnj1373  33019  lfuhgr2  33089  lfuhgr3  33090  acycgr1v  33120  umgracycusgr  33125  cusgracyclt3v  33127  dmopab3rexdif  33376  xpord2pred  33801  xpord3pred  33807  wzel  33827  dfrdg4  34262  bj-sbeq  35095  bj-sbel1  35099  bj-snsetex  35162  bj-snglc  35168  bj-taginv  35185  poimirlem16  35802  poimirlem19  35805  eldmres  36416  ecres  36421  ecres2  36422  eldmqsres  36429  inxprnres  36435  cnvepres  36441  idinxpss  36455  inxpssidinxp  36458  idinxpssinxp  36459  alrmomorn  36497  alrmomodm  36498  brxrn  36511  dfxrn2  36513  inxpxrn  36528  rnxrn  36531  rnxrnres  36532  rnxrncnvepres  36533  rnxrnidres  36534  1cossres  36559  dfcoels  36560  br1cossinidres  36574  br1cossincnvepres  36575  br1cossxrnidres  36576  br1cossxrncnvepres  36577  refrelcosslem  36587  coss0  36604  cossid  36605  br1cossxrncnvssrres  36633  dfrefrels2  36638  dfcnvrefrels2  36651  dfcnvrefrels3  36652  dfsymrels2  36666  dftrrels2  36696  eldmqs1cossres  36778  dfeldisj5  36839  prter2  36902  cdleme31sdnN  38408  sn-iotalem  40196  iotavallem  40199  inintabss  41193  inintabd  41194  cnvcnvintabd  41215  cnvintabd  41218  comptiunov2i  41321  cotrcltrcl  41340  corcltrcl  41354  cotrclrcl  41357  rr-grothprimbi  41920  rr-groth  41924  dfuniv2  41927  onfrALTlem4VD  42513  iinssiin  42685  iinssf  42694  rnmptpr  42720  wessf1ornlem  42729  disjinfi  42738  rnmptlb  42795  rnmptbddlem  42796  rnmptbd2lem  42801  ellimcabssub0  43165  eusnsn  44531  dfdfat2  44631  mofeu  46186  onsetreclem1  46421