Theorem elv 3460

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  csbconstg  3872  csbvarg  4399  iinconst  4967  iuniin  4969  iinssiun  4970  iinss1  4972  ssiinf  5019  iinss  5021  iinss2  5022  iinab  5032  iinun2  5037  iundif2  5038  iindif1  5041  iindif2  5043  iinin2  5044  iinpw  5072  brab1  5159  triin  5235  eusvnf  5363  sbcop  5471  iunopab  5544  pwvabrel  5712  ssrel  5769  xpiindi  5821  cnv0  5869  dmopab2rex  5907  dfima2  6064  args  6094  inisegn0  6100  dffr3  6101  dfse2  6102  dfco2a  6247  dfpo2  6297  iotaval2  6507  iinpreima  7064  tfinds2  7856  fvresex  7953  sbcoteq1a  8044  fnse  8125  xpord2pred  8137  xpord3lem  8141  xpord3pred  8144  suppvalbr  8156  cnvimadfsn  8164  reldmtpos  8226  rntpos  8231  ovtpos  8233  dftpos3  8236  tpostpos  8238  fprlem2  8294  onovuni  8325  oarec  8543  eqerlem  8726  elecreseq  8740  ixpiin  8918  ixpsnf1o  8932  boxriin  8934  idssen  8990  unxpdomlem3  9214  ac6sfi  9240  unbnn2  9253  fifo  9388  inf0  9586  ttrclselem2  9691  ttrclse  9692  rankxpsuc  9850  tcrank  9852  harcard  9960  infxpenlem  9993  infpwfien  10042  alephcard  10050  dfac3  10101  cflm  10228  fin23lem34  10325  dffin7-2  10377  fin1a2lem13  10391  itunitc1  10399  itunitc  10400  ituniiun  10401  hsmexlem4  10408  fin41  10423  axdclem2  10499  fpwwe2lem11  10621  fpwwe2lem12  10622  fpwwe2  10623  canthwe  10631  pwfseqlem5  10643  axgroth2  10805  axgroth6  10808  grothac  10810  grothtsk  10815  seqfeq4  14083  serle  14089  seqof  14091  hash1snb  14452  hashmap  14468  hashfun  14470  hashbclem  14485  hashf1lem2  14489  hashf1  14490  hash2prde  14503  prprrab  14506  hash3tpexb  14527  fi1uzind  14540  brfi1indALT  14543  s3sndisj  15000  s3iunsndisj  15001  rexfiuz  15395  fsumabs  15849  incexclem  15886  fprodcllemf  16008  fprodmodd  16047  iserodd  16890  hashbc0  17060  0ram  17075  ramub1  17083  initoid  18053  termoid  18054  equivestrcsetc  18203  gsumwspan  18900  gsmsymgrfix  19493  symgfixf1  19502  frgpnabllem1  19938  telgsums  20058  opprsubg  20430  subrngpropd  20667  subrgpropd  20707  coe1fzgsumdlem  22463  evl1gsumdlem  22516  mdetunilem9  22777  topnex  23153  neitr  23337  ordtbas2  23348  pnfnei  23377  mnfnei  23378  hauscmplem  23563  2ndcsb  23606  2ndcsep  23616  ptpjopn  23769  snfil  24021  fbasrn  24041  rnelfmlem  24109  rnelfm  24110  fmfnfmlem3  24113  fmfnfmlem4  24114  fmfnfm  24115  fclscmp  24187  alexsubALTlem4  24207  ptcmplem2  24210  symgtgp  24263  ustfilxp  24370  restutopopn  24395  ustuqtop2  24399  utopsnneiplem  24404  imasdsf1olem  24530  xpsdsval  24538  metuel2  24722  metustbl  24723  restmetu  24727  xrtgioo  24964  minveclem3b  25587  ovoliunlem1  25661  uniioombllem3  25744  itg1addlem4  25858  dvnff  26082  dvfsumlem3  26187  logfac  26766  gausslemma2dlem1a  27529  onsis  28467  ons2ind  28468  umgrislfupgrlem  29472  lfuhgr1v0e  29604  cplgrop  29787  finsumvtxdg2size  29900  rgrusgrprc  29939  elwspths2spth  30319  fusgr2wsp2nb  30685  h2hlm  31332  axhcompl-zf  31350  opsbc2ie  32822  inpr0  32878  iuninc  32905  disjpreima  32929  suppss2f  32983  fnpreimac  33015  tocyccntz  33464  elrgspnlem1  33562  elrgspnlem2  33563  nsgqusf1olem2  33723  nsgqusf1olem3  33724  zarclsiin  34261  esumpfinvalf  34466  measiuns  34607  bnj23  35107  bnj110  35246  bnj1123  35374  bnj1373  35418  fineqvnttrclse  35537  kardeq0  35569  lfuhgr2  35611  lfuhgr3  35612  acycgr1v  35641  umgracycusgr  35646  cusgracyclt3v  35648  dmopab3rexdif  35897  wzel  36314  dfrdg4  36443  bj-sbeq  37536  bj-sbel1  37540  bj-snsetex  37599  bj-snglc  37605  bj-taginv  37622  bj-adjfrombun  37682  poimirlem16  38287  poimirlem19  38290  eldmres  38926  ecres  38934  eldmqsres  38942  inxprnres  38947  cnvepres  38953  idinxpss  38967  inxpssidinxp  38971  idinxpssinxp  38972  cnvref5  39000  alrmomorn  39007  alrmomodm  39008  ssdmral  39028  brxrn  39032  dfxrn2  39034  dmcnvep  39037  inxpxrn  39067  rnxrn  39070  rnxrnres  39071  rnxrncnvepres  39072  rnxrnidres  39073  blockadjliftmap  39107  dfsucmap3  39112  dmsucmap  39117  dfsuccl4  39123  coss1cnvres  39156  coss2cnvepres  39157  1cossres  39168  dfcoels  39169  refressn  39182  br1cossinidres  39188  br1cossincnvepres  39189  br1cossxrnidres  39190  br1cossxrncnvepres  39191  refrelcosslem  39201  coss0  39218  cossid  39219  br1cossxrncnvssrres  39237  dfrefrels2  39242  dfcnvrefrels2  39257  dfcnvrefrels3  39258  dfsymrels2  39274  dftrrels2  39308  eldmqs1cossres  39393  disjimdmqseq  39458  dfeldisj5  39462  eldisjdmqsim  39466  disjres  39493  antisymrelres  39515  disjdmqsss  39554  disjdmqscossss  39555  mpets  39605  dmqsblocks  39616  dfpeters2  39623  prter2  39655  cdleme31sdnN  41161  evl1gprodd  42884  sn-iotalem  42992  inintabss  44304  inintabd  44305  cnvcnvintabd  44326  cnvintabd  44329  comptiunov2i  44432  cotrcltrcl  44451  corcltrcl  44465  cotrclrcl  44468  rr-grothprimbi  45005  rr-groth  45009  dfuniv2  45012  onfrALTlem4VD  45594  iinssiin  45847  iinssf  45856  iindif2f  45878  rnmptpr  45895  wessf1ornlem  45903  disjinfi  45910  rnmptlb  45958  rnmptbddlem  45959  rnmptbd2lem  45963  ellimcabssub0  46333  preimageiingt  47434  preimaleiinlt  47435  eusnsn  47763  dfdfat2  47865  iineq0  49598  iinxp  49609  mofeu  49626  tposres0  49655  iinfsubc  49836  onsetreclem1  50483