Theorem elv 3481

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  csbconstg  3911  csbvarg  4430  iinconst  5006  iuniin  5008  iinssiun  5009  iinss1  5011  ssiinf  5056  iinss  5058  iinss2  5059  iinab  5070  iinun2  5075  iundif2  5076  iindif1  5077  iindif2  5079  iinin2  5080  iinpw  5108  brab1  5195  triin  5281  eusvnf  5389  sbcop  5488  iunopab  5558  pwvabrel  5725  ssrel  5780  difopabOLD  5829  xpiindi  5833  dmopab2rex  5915  dfima2  6059  args  6088  inisegn0  6094  dffr3  6095  dfse2  6096  dfco2a  6242  dfpo2  6292  iotaval2  6508  iotavalOLD  6514  iinpreima  7066  tfinds2  7848  fvresex  7941  sbcoteq1a  8032  fnse  8114  xpord2pred  8126  xpord3lem  8130  xpord3pred  8133  suppvalbr  8145  cnvimadfsn  8152  reldmtpos  8214  rntpos  8219  ovtpos  8221  dftpos3  8224  tpostpos  8226  fprlem2  8281  wfrlem10OLD  8313  onovuni  8337  oarec  8558  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  14013  serle  14019  seqof  14021  hash1snb  14375  hashmap  14391  hashfun  14393  hashbclem  14407  hashf1lem2  14413  hashf1  14414  hash2prde  14427  prprrab  14430  fi1uzind  14454  brfi1indALT  14457  s3sndisj  14910  s3iunsndisj  14911  rexfiuz  15290  fsumabs  15743  incexclem  15778  fprodcllemf  15898  fprodmodd  15937  iserodd  16764  hashbc0  16934  0ram  16949  ramub1  16957  initoid  17947  termoid  17948  equivestrcsetc  18100  gsumwspan  18723  gsmsymgrfix  19289  symgfixf1  19298  frgpnabllem1  19733  telgsums  19853  opprsubg  20155  subrgpropd  20388  coe1fzgsumdlem  21807  evl1gsumdlem  21857  mdetunilem9  22104  topnex  22481  neitr  22666  ordtbas2  22677  pnfnei  22706  mnfnei  22707  hauscmplem  22892  2ndcsb  22935  2ndcsep  22945  ptpjopn  23098  snfil  23350  fbasrn  23370  rnelfmlem  23438  rnelfm  23439  fmfnfmlem3  23442  fmfnfmlem4  23443  fmfnfm  23444  fclscmp  23516  alexsubALTlem4  23536  ptcmplem2  23539  symgtgp  23592  ustfilxp  23699  restutopopn  23725  ustuqtop2  23729  utopsnneiplem  23734  imasdsf1olem  23861  xpsdsval  23869  metuel2  24056  metustbl  24057  restmetu  24061  xrtgioo  24304  minveclem3b  24927  ovoliunlem1  25001  uniioombllem3  25084  itg1addlem4  25198  itg1addlem4OLD  25199  dvnff  25422  dvfsumlem3  25527  logfac  26091  gausslemma2dlem1a  26848  umgrislfupgrlem  28362  lfuhgr1v0e  28491  cplgrop  28674  finsumvtxdg2size  28787  rgrusgrprc  28826  elwspths2spth  29201  fusgr2wsp2nb  29567  h2hlm  30211  axhcompl-zf  30229  opsbc2ie  31694  inpr0  31747  iuninc  31770  disjpreima  31793  suppss2f  31841  fnpreimac  31874  tocyccntz  32281  nsgqusf1olem2  32488  nsgqusf1olem3  32489  zarclsiin  32789  esumpfinvalf  33012  measiuns  33153  bnj23  33667  bnj110  33807  bnj1123  33935  bnj1373  33979  lfuhgr2  34047  lfuhgr3  34048  acycgr1v  34078  umgracycusgr  34083  cusgracyclt3v  34085  dmopab3rexdif  34334  wzel  34734  dfrdg4  34861  bj-sbeq  35719  bj-sbel1  35723  bj-snsetex  35782  bj-snglc  35788  bj-taginv  35805  bj-adjfrombun  35865  poimirlem16  36442  poimirlem19  36445  eldmres  37076  ecres  37084  ecres2  37085  eldmqsres  37093  inxprnres  37099  cnvepres  37105  idinxpss  37119  inxpssidinxp  37123  idinxpssinxp  37124  cnvref5  37158  alrmomorn  37165  alrmomodm  37166  brxrn  37182  dfxrn2  37184  inxpxrn  37203  rnxrn  37206  rnxrnres  37207  rnxrncnvepres  37208  rnxrnidres  37209  coss1cnvres  37225  coss2cnvepres  37226  1cossres  37237  dfcoels  37238  refressn  37251  br1cossinidres  37257  br1cossincnvepres  37258  br1cossxrnidres  37259  br1cossxrncnvepres  37260  refrelcosslem  37270  coss0  37287  cossid  37288  br1cossxrncnvssrres  37316  dfrefrels2  37321  dfcnvrefrels2  37336  dfcnvrefrels3  37337  dfsymrels2  37353  dftrrels2  37383  eldmqs1cossres  37467  dfeldisj5  37529  disjres  37552  antisymrelres  37571  disjdmqsss  37610  disjdmqscossss  37611  mpets  37650  prter2  37689  cdleme31sdnN  39196  sn-iotalem  40986  inintabss  42262  inintabd  42263  cnvcnvintabd  42284  cnvintabd  42287  comptiunov2i  42390  cotrcltrcl  42409  corcltrcl  42423  cotrclrcl  42426  rr-grothprimbi  42987  rr-groth  42991  dfuniv2  42994  onfrALTlem4VD  43580  iinssiin  43751  iinssf  43760  iindif2f  43787  rnmptpr  43806  wessf1ornlem  43815  disjinfi  43824  rnmptlb  43881  rnmptbddlem  43882  rnmptbd2lem  43887  ellimcabssub0  44268  eusnsn  45671  dfdfat2  45771  subrngpropd  46680  mofeu  47416  onsetreclem1  47652