Theorem elv 3479

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475

This theorem is referenced by:  csbconstg  3912  csbvarg  4431  iinconst  5007  iuniin  5009  iinssiun  5010  iinss1  5012  ssiinf  5057  iinss  5059  iinss2  5060  iinab  5071  iinun2  5076  iundif2  5077  iindif1  5078  iindif2  5080  iinin2  5081  iinpw  5109  brab1  5196  triin  5282  eusvnf  5390  sbcop  5489  iunopab  5559  pwvabrel  5727  ssrel  5782  difopabOLD  5831  xpiindi  5835  dmopab2rex  5917  dfima2  6061  args  6091  inisegn0  6097  dffr3  6098  dfse2  6099  dfco2a  6245  dfpo2  6295  iotaval2  6511  iotavalOLD  6517  iinpreima  7070  tfinds2  7857  fvresex  7950  sbcoteq1a  8041  fnse  8123  xpord2pred  8135  xpord3lem  8139  xpord3pred  8142  suppvalbr  8154  cnvimadfsn  8161  reldmtpos  8223  rntpos  8228  ovtpos  8230  dftpos3  8233  tpostpos  8235  fprlem2  8290  wfrlem10OLD  8322  onovuni  8346  oarec  8566  eqerlem  8741  ixpiin  8922  ixpsnf1o  8936  boxriin  8938  idssen  8997  unxpdomlem3  9256  ac6sfi  9291  unbnn2  9304  fifo  9431  inf0  9620  ttrclselem2  9725  ttrclse  9726  rankxpsuc  9881  tcrank  9883  harcard  9977  infxpenlem  10012  infpwfien  10061  alephcard  10069  dfac3  10120  cflm  10249  fin23lem34  10345  dffin7-2  10397  fin1a2lem13  10411  itunitc1  10419  itunitc  10420  ituniiun  10421  hsmexlem4  10428  fin41  10443  axdclem2  10519  fpwwe2lem11  10640  fpwwe2lem12  10641  fpwwe2  10642  canthwe  10650  pwfseqlem5  10662  axgroth2  10824  axgroth6  10827  grothac  10829  grothtsk  10834  seqfeq4  14022  serle  14028  seqof  14030  hash1snb  14384  hashmap  14400  hashfun  14402  hashbclem  14416  hashf1lem2  14422  hashf1  14423  hash2prde  14436  prprrab  14439  fi1uzind  14463  brfi1indALT  14466  s3sndisj  14919  s3iunsndisj  14920  rexfiuz  15299  fsumabs  15752  incexclem  15787  fprodcllemf  15907  fprodmodd  15946  iserodd  16773  hashbc0  16943  0ram  16958  ramub1  16966  initoid  17956  termoid  17957  equivestrcsetc  18109  gsumwspan  18764  gsmsymgrfix  19338  symgfixf1  19347  frgpnabllem1  19783  telgsums  19903  opprsubg  20244  subrngpropd  20457  subrgpropd  20499  coe1fzgsumdlem  22046  evl1gsumdlem  22096  mdetunilem9  22343  topnex  22720  neitr  22905  ordtbas2  22916  pnfnei  22945  mnfnei  22946  hauscmplem  23131  2ndcsb  23174  2ndcsep  23184  ptpjopn  23337  snfil  23589  fbasrn  23609  rnelfmlem  23677  rnelfm  23678  fmfnfmlem3  23681  fmfnfmlem4  23682  fmfnfm  23683  fclscmp  23755  alexsubALTlem4  23775  ptcmplem2  23778  symgtgp  23831  ustfilxp  23938  restutopopn  23964  ustuqtop2  23968  utopsnneiplem  23973  imasdsf1olem  24100  xpsdsval  24108  metuel2  24295  metustbl  24296  restmetu  24300  xrtgioo  24543  minveclem3b  25177  ovoliunlem1  25252  uniioombllem3  25335  itg1addlem4  25449  itg1addlem4OLD  25450  dvnff  25674  dvfsumlem3  25781  logfac  26346  gausslemma2dlem1a  27105  umgrislfupgrlem  28650  lfuhgr1v0e  28779  cplgrop  28962  finsumvtxdg2size  29075  rgrusgrprc  29114  elwspths2spth  29489  fusgr2wsp2nb  29855  h2hlm  30501  axhcompl-zf  30519  opsbc2ie  31984  inpr0  32037  iuninc  32060  disjpreima  32083  suppss2f  32131  fnpreimac  32164  tocyccntz  32574  nsgqusf1olem2  32800  nsgqusf1olem3  32801  zarclsiin  33150  esumpfinvalf  33373  measiuns  33514  bnj23  34028  bnj110  34168  bnj1123  34296  bnj1373  34340  lfuhgr2  34408  lfuhgr3  34409  acycgr1v  34439  umgracycusgr  34444  cusgracyclt3v  34446  dmopab3rexdif  34695  wzel  35101  dfrdg4  35228  bj-sbeq  36085  bj-sbel1  36089  bj-snsetex  36148  bj-snglc  36154  bj-taginv  36171  bj-adjfrombun  36231  poimirlem16  36808  poimirlem19  36811  eldmres  37442  ecres  37450  ecres2  37451  eldmqsres  37459  inxprnres  37465  cnvepres  37471  idinxpss  37485  inxpssidinxp  37489  idinxpssinxp  37490  cnvref5  37524  alrmomorn  37531  alrmomodm  37532  brxrn  37548  dfxrn2  37550  inxpxrn  37569  rnxrn  37572  rnxrnres  37573  rnxrncnvepres  37574  rnxrnidres  37575  coss1cnvres  37591  coss2cnvepres  37592  1cossres  37603  dfcoels  37604  refressn  37617  br1cossinidres  37623  br1cossincnvepres  37624  br1cossxrnidres  37625  br1cossxrncnvepres  37626  refrelcosslem  37636  coss0  37653  cossid  37654  br1cossxrncnvssrres  37682  dfrefrels2  37687  dfcnvrefrels2  37702  dfcnvrefrels3  37703  dfsymrels2  37719  dftrrels2  37749  eldmqs1cossres  37833  dfeldisj5  37895  disjres  37918  antisymrelres  37937  disjdmqsss  37976  disjdmqscossss  37977  mpets  38016  prter2  38055  cdleme31sdnN  39562  sn-iotalem  41345  inintabss  42632  inintabd  42633  cnvcnvintabd  42654  cnvintabd  42657  comptiunov2i  42760  cotrcltrcl  42779  corcltrcl  42793  cotrclrcl  42796  rr-grothprimbi  43357  rr-groth  43361  dfuniv2  43364  onfrALTlem4VD  43950  iinssiin  44120  iinssf  44129  iindif2f  44156  rnmptpr  44175  wessf1ornlem  44183  disjinfi  44190  rnmptlb  44246  rnmptbddlem  44247  rnmptbd2lem  44251  ellimcabssub0  44632  eusnsn  46035  dfdfat2  46135  mofeu  47602  onsetreclem1  47838