Theorem elv 3499

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  csbvarg  4382  iinconst  4928  iuniin  4930  iinssiun  4931  iinss1  4933  ssiinf  4977  iinss  4979  iinss2  4980  iinab  4989  iinun2  4994  iundif2  4995  iindif1  4996  iindif2  4998  iinin2  4999  iinpw  5027  brab1  5113  triin  5186  eusvnf  5292  sbcop  5379  pwvabrel  5602  difopab  5701  xpiindi  5705  dmopab2rex  5785  dfima2  5930  args  5956  inisegn0  5960  dffr3  5961  dfse2  5962  dfco2a  6098  iotaval  6328  iinpreima  6836  tfinds2  7577  fvresex  7660  fnse  7826  suppvalbr  7833  cnvimadfsn  7838  reldmtpos  7899  rntpos  7904  ovtpos  7906  dftpos3  7909  tpostpos  7911  wfrlem10  7963  onovuni  7978  oarec  8187  eqerlem  8322  ixpiin  8487  ixpsnf1o  8501  boxriin  8503  idssen  8553  unxpdomlem3  8723  ac6sfi  8761  unbnn2  8774  fifo  8895  inf0  9083  rankxpsuc  9310  tcrank  9312  harcard  9406  infxpenlem  9438  infpwfien  9487  alephcard  9495  dfac3  9546  cflm  9671  fin23lem34  9767  dffin7-2  9819  fin1a2lem13  9833  itunitc1  9841  itunitc  9842  ituniiun  9843  hsmexlem4  9850  fin41  9865  axdclem2  9941  fpwwe2lem12  10062  fpwwe2lem13  10063  fpwwe2  10064  canthwe  10072  pwfseqlem5  10084  axgroth2  10246  axgroth6  10249  grothac  10251  grothtsk  10256  seqfeq4  13418  serle  13424  seqof  13426  hash1snb  13779  hashmap  13795  hashfun  13797  hashbclem  13809  hashf1lem2  13813  hashf1  13814  hash2prde  13827  prprrab  13830  fi1uzind  13854  s3sndisj  14326  s3iunsndisj  14327  rexfiuz  14706  fsumabs  15155  incexclem  15190  fprodcllemf  15311  fprodmodd  15350  iserodd  16171  hashbc0  16340  0ram  16355  ramub1  16363  initoid  17264  termoid  17265  equivestrcsetc  17401  gsumwspan  18010  gsmsymgrfix  18555  symgfixf1  18564  frgpnabllem1  18992  telgsums  19112  opprsubg  19385  subrgpropd  19569  coe1fzgsumdlem  20468  evl1gsumdlem  20518  mdetunilem9  21228  topnex  21603  neitr  21787  ordtbas2  21798  pnfnei  21827  mnfnei  21828  hauscmplem  22013  2ndcsb  22056  2ndcsep  22066  ptpjopn  22219  snfil  22471  fbasrn  22491  rnelfmlem  22559  rnelfm  22560  fmfnfmlem3  22563  fmfnfmlem4  22564  fmfnfm  22565  fclscmp  22637  alexsubALTlem4  22657  ptcmplem2  22660  symgtgp  22713  ustfilxp  22820  restutopopn  22846  ustuqtop2  22850  utopsnneiplem  22855  imasdsf1olem  22982  xpsdsval  22990  metuel2  23174  metustbl  23175  restmetu  23179  xrtgioo  23413  minveclem3b  24030  ovoliunlem1  24102  uniioombllem3  24185  itg1addlem4  24299  dvnff  24519  dvfsumlem3  24624  logfac  25183  gausslemma2dlem1a  25940  umgrislfupgrlem  26906  lfuhgr1v0e  27035  cplgrop  27218  finsumvtxdg2size  27331  rgrusgrprc  27370  elwspths2spth  27745  fusgr2wsp2nb  28112  h2hlm  28756  axhcompl-zf  28774  opsbc2ie  30238  inpr0  30291  iuninc  30311  disjpreima  30333  suppss2f  30383  fnpreimac  30415  tocyccntz  30786  esumpfinvalf  31335  measiuns  31476  bnj23  31988  bnj110  32130  bnj1123  32258  bnj1373  32302  lfuhgr2  32365  lfuhgr3  32366  acycgr1v  32396  umgracycusgr  32401  cusgracyclt3v  32403  dmopab3rexdif  32652  dfpo2  32991  wzel  33111  fprlem2  33138  dfrdg4  33412  bj-sbeq  34218  bj-sbel1  34222  bj-snsetex  34275  bj-snglc  34281  bj-taginv  34298  eldmres  35529  ecres  35534  ecres2  35535  eldmqsres  35542  inxprnres  35548  cnvepres  35554  idinxpss  35569  inxpssidinxp  35572  idinxpssinxp  35573  alrmomorn  35611  alrmomodm  35612  brxrn  35625  dfxrn2  35627  inxpxrn  35642  rnxrn  35645  rnxrnres  35646  rnxrncnvepres  35647  rnxrnidres  35648  1cossres  35673  dfcoels  35674  br1cossinidres  35688  br1cossincnvepres  35689  br1cossxrnidres  35690  br1cossxrncnvepres  35691  refrelcosslem  35701  coss0  35718  cossid  35719  br1cossxrncnvssrres  35747  dfrefrels2  35752  dfcnvrefrels2  35765  dfcnvrefrels3  35766  dfsymrels2  35780  dftrrels2  35810  eldmqs1cossres  35892  dfeldisj5  35953  prter2  36016  cdleme31sdnN  37522  inintabss  39936  inintabd  39937  cnvcnvintabd  39958  cnvintabd  39961  comptiunov2i  40049  cotrcltrcl  40068  corcltrcl  40082  cotrclrcl  40085  rr-grothprimbi  40629  rr-groth  40633  onfrALTlem4VD  41218  iinssiin  41393  iinssf  41405  rnmptpr  41431  wessf1ornlem  41443  rnmptlb  41512  rnmptbddlem  41513  rnmptbd2lem  41518  ellimcabssub0  41896  eusnsn  43260  dfdfat2  43326  onsetreclem1  44806