Theorem elv 3435

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  csbconstg  3857  csbvarg  4375  iinconst  4945  iuniin  4947  iinssiun  4948  iinss1  4950  ssiinf  4998  iinss  5000  iinss2  5001  iinab  5011  iinun2  5016  iundif2  5017  iindif1  5018  iindif2  5020  iinin2  5021  iinpw  5049  brab1  5134  triin  5210  eusvnf  5330  sbcop  5438  iunopab  5508  pwvabrel  5676  ssrel  5733  xpiindi  5785  dmopab2rex  5867  dfima2  6022  args  6052  inisegn0  6058  dffr3  6059  dfse2  6060  cnv0  6098  dfco2a  6205  dfpo2  6255  iotaval2  6464  iinpreima  7016  tfinds2  7809  fvresex  7907  sbcoteq1a  7998  fnse  8077  xpord2pred  8089  xpord3lem  8093  xpord3pred  8096  suppvalbr  8108  cnvimadfsn  8116  reldmtpos  8178  rntpos  8183  ovtpos  8185  dftpos3  8188  tpostpos  8190  fprlem2  8245  onovuni  8276  oarec  8491  eqerlem  8673  elecreseq  8687  ixpiin  8866  ixpsnf1o  8880  boxriin  8882  idssen  8938  unxpdomlem3  9162  ac6sfi  9188  unbnn2  9201  fifo  9339  inf0  9536  ttrclselem2  9641  ttrclse  9642  rankxpsuc  9800  tcrank  9802  harcard  9896  infxpenlem  9929  infpwfien  9978  alephcard  9986  dfac3  10037  cflm  10166  fin23lem34  10262  dffin7-2  10314  fin1a2lem13  10328  itunitc1  10336  itunitc  10337  ituniiun  10338  hsmexlem4  10345  fin41  10360  axdclem2  10436  fpwwe2lem11  10558  fpwwe2lem12  10559  fpwwe2  10560  canthwe  10568  pwfseqlem5  10580  axgroth2  10742  axgroth6  10745  grothac  10747  grothtsk  10752  seqfeq4  14007  serle  14013  seqof  14015  hash1snb  14375  hashmap  14391  hashfun  14393  hashbclem  14408  hashf1lem2  14412  hashf1  14413  hash2prde  14426  prprrab  14429  hash3tpexb  14450  fi1uzind  14463  brfi1indALT  14466  s3sndisj  14923  s3iunsndisj  14924  rexfiuz  15304  fsumabs  15758  incexclem  15795  fprodcllemf  15917  fprodmodd  15956  iserodd  16800  hashbc0  16970  0ram  16985  ramub1  16993  initoid  17962  termoid  17963  equivestrcsetc  18112  gsumwspan  18808  gsmsymgrfix  19397  symgfixf1  19406  frgpnabllem1  19842  telgsums  19962  opprsubg  20326  subrngpropd  20539  subrgpropd  20579  coe1fzgsumdlem  22281  evl1gsumdlem  22334  mdetunilem9  22598  topnex  22974  neitr  23158  ordtbas2  23169  pnfnei  23198  mnfnei  23199  hauscmplem  23384  2ndcsb  23427  2ndcsep  23437  ptpjopn  23590  snfil  23842  fbasrn  23862  rnelfmlem  23930  rnelfm  23931  fmfnfmlem3  23934  fmfnfmlem4  23935  fmfnfm  23936  fclscmp  24008  alexsubALTlem4  24028  ptcmplem2  24031  symgtgp  24084  ustfilxp  24191  restutopopn  24216  ustuqtop2  24220  utopsnneiplem  24225  imasdsf1olem  24351  xpsdsval  24359  metuel2  24543  metustbl  24544  restmetu  24548  xrtgioo  24785  minveclem3b  25408  ovoliunlem1  25482  uniioombllem3  25565  itg1addlem4  25679  dvnff  25903  dvfsumlem3  26008  logfac  26581  gausslemma2dlem1a  27345  onsis  28283  ons2ind  28284  umgrislfupgrlem  29208  lfuhgr1v0e  29340  cplgrop  29523  finsumvtxdg2size  29637  rgrusgrprc  29676  elwspths2spth  30056  fusgr2wsp2nb  30422  h2hlm  31069  axhcompl-zf  31087  opsbc2ie  32563  inpr0  32620  iuninc  32648  disjpreima  32672  suppss2f  32729  fnpreimac  32761  tocyccntz  33223  elrgspnlem1  33321  elrgspnlem2  33322  nsgqusf1olem2  33492  nsgqusf1olem3  33493  zarclsiin  34034  esumpfinvalf  34239  measiuns  34380  bnj23  34880  bnj110  35019  bnj1123  35147  bnj1373  35191  fineqvnttrclse  35287  lfuhgr2  35320  lfuhgr3  35321  acycgr1v  35350  umgracycusgr  35355  cusgracyclt3v  35357  dmopab3rexdif  35606  wzel  36023  dfrdg4  36152  bj-sbeq  37227  bj-sbel1  37231  bj-snsetex  37289  bj-snglc  37295  bj-taginv  37312  bj-adjfrombun  37372  poimirlem16  37974  poimirlem19  37977  eldmres  38615  ecres  38623  eldmqsres  38631  inxprnres  38636  cnvepres  38642  idinxpss  38656  inxpssidinxp  38660  idinxpssinxp  38661  cnvref5  38689  alrmomorn  38696  alrmomodm  38697  ssdmral  38717  brxrn  38721  dfxrn2  38723  dmcnvep  38726  inxpxrn  38756  rnxrn  38759  rnxrnres  38760  rnxrncnvepres  38761  rnxrnidres  38762  blockadjliftmap  38796  dfsucmap3  38801  dmsucmap  38806  dfsuccl4  38812  coss1cnvres  38845  coss2cnvepres  38846  1cossres  38857  dfcoels  38858  refressn  38871  br1cossinidres  38877  br1cossincnvepres  38878  br1cossxrnidres  38879  br1cossxrncnvepres  38880  refrelcosslem  38890  coss0  38907  cossid  38908  br1cossxrncnvssrres  38926  dfrefrels2  38931  dfcnvrefrels2  38946  dfcnvrefrels3  38947  dfsymrels2  38963  dftrrels2  38997  eldmqs1cossres  39082  disjimdmqseq  39147  dfeldisj5  39151  eldisjdmqsim  39155  disjres  39182  antisymrelres  39204  disjdmqsss  39243  disjdmqscossss  39244  mpets  39294  dmqsblocks  39305  dfpeters2  39312  prter2  39344  cdleme31sdnN  40850  evl1gprodd  42573  sn-iotalem  42679  inintabss  44026  inintabd  44027  cnvcnvintabd  44048  cnvintabd  44051  comptiunov2i  44154  cotrcltrcl  44173  corcltrcl  44187  cotrclrcl  44190  rr-grothprimbi  44743  rr-groth  44747  dfuniv2  44750  onfrALTlem4VD  45333  iinssiin  45580  iinssf  45589  iindif2f  45611  rnmptpr  45628  wessf1ornlem  45636  disjinfi  45643  rnmptlb  45693  rnmptbddlem  45694  rnmptbd2lem  45698  ellimcabssub0  46068  preimageiingt  47169  preimaleiinlt  47170  eusnsn  47489  dfdfat2  47591  iineq0  49310  iinxp  49321  mofeu  49338  tposres0  49367  iinfsubc  49548  onsetreclem1  50195