Theorem elv 3452

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449

This theorem is referenced by:  csbconstg  3881  csbvarg  4397  iinconst  4966  iuniin  4968  iinssiun  4969  iinss1  4971  ssiinf  5018  iinss  5020  iinss2  5021  iinab  5032  iinun2  5037  iundif2  5038  iindif1  5039  iindif2  5041  iinin2  5042  iinpw  5070  brab1  5155  triin  5231  eusvnf  5347  sbcop  5449  iunopab  5519  pwvabrel  5689  ssrel  5745  difopabOLD  5794  xpiindi  5799  dmopab2rex  5881  dfima2  6033  args  6063  inisegn0  6069  dffr3  6070  dfse2  6071  dfco2a  6219  dfpo2  6269  iotaval2  6479  iotavalOLD  6485  iinpreima  7041  tfinds2  7840  fvresex  7938  sbcoteq1a  8030  fnse  8112  xpord2pred  8124  xpord3lem  8128  xpord3pred  8131  suppvalbr  8143  cnvimadfsn  8151  reldmtpos  8213  rntpos  8218  ovtpos  8220  dftpos3  8223  tpostpos  8225  fprlem2  8280  onovuni  8311  oarec  8526  eqerlem  8706  elecreseq  8720  ixpiin  8897  ixpsnf1o  8911  boxriin  8913  idssen  8968  unxpdomlem3  9199  ac6sfi  9231  unbnn2  9244  fifo  9383  inf0  9574  ttrclselem2  9679  ttrclse  9680  rankxpsuc  9835  tcrank  9837  harcard  9931  infxpenlem  9966  infpwfien  10015  alephcard  10023  dfac3  10074  cflm  10203  fin23lem34  10299  dffin7-2  10351  fin1a2lem13  10365  itunitc1  10373  itunitc  10374  ituniiun  10375  hsmexlem4  10382  fin41  10397  axdclem2  10473  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  canthwe  10604  pwfseqlem5  10616  axgroth2  10778  axgroth6  10781  grothac  10783  grothtsk  10788  seqfeq4  14016  serle  14022  seqof  14024  hash1snb  14384  hashmap  14400  hashfun  14402  hashbclem  14417  hashf1lem2  14421  hashf1  14422  hash2prde  14435  prprrab  14438  hash3tpexb  14459  fi1uzind  14472  brfi1indALT  14475  s3sndisj  14933  s3iunsndisj  14934  rexfiuz  15314  fsumabs  15767  incexclem  15802  fprodcllemf  15924  fprodmodd  15963  iserodd  16806  hashbc0  16976  0ram  16991  ramub1  16999  initoid  17963  termoid  17964  equivestrcsetc  18113  gsumwspan  18773  gsmsymgrfix  19358  symgfixf1  19367  frgpnabllem1  19803  telgsums  19923  opprsubg  20261  subrngpropd  20477  subrgpropd  20517  coe1fzgsumdlem  22190  evl1gsumdlem  22243  mdetunilem9  22507  topnex  22883  neitr  23067  ordtbas2  23078  pnfnei  23107  mnfnei  23108  hauscmplem  23293  2ndcsb  23336  2ndcsep  23346  ptpjopn  23499  snfil  23751  fbasrn  23771  rnelfmlem  23839  rnelfm  23840  fmfnfmlem3  23843  fmfnfmlem4  23844  fmfnfm  23845  fclscmp  23917  alexsubALTlem4  23937  ptcmplem2  23940  symgtgp  23993  ustfilxp  24100  restutopopn  24126  ustuqtop2  24130  utopsnneiplem  24135  imasdsf1olem  24261  xpsdsval  24269  metuel2  24453  metustbl  24454  restmetu  24458  xrtgioo  24695  minveclem3b  25328  ovoliunlem1  25403  uniioombllem3  25486  itg1addlem4  25600  dvnff  25825  dvfsumlem3  25935  logfac  26510  gausslemma2dlem1a  27276  onsis  28172  umgrislfupgrlem  29049  lfuhgr1v0e  29181  cplgrop  29364  finsumvtxdg2size  29478  rgrusgrprc  29517  elwspths2spth  29897  fusgr2wsp2nb  30263  h2hlm  30909  axhcompl-zf  30927  opsbc2ie  32405  inpr0  32461  iuninc  32489  disjpreima  32513  suppss2f  32562  fnpreimac  32595  tocyccntz  33101  elrgspnlem1  33193  elrgspnlem2  33194  nsgqusf1olem2  33385  nsgqusf1olem3  33386  zarclsiin  33861  esumpfinvalf  34066  measiuns  34207  bnj23  34708  bnj110  34848  bnj1123  34976  bnj1373  35020  lfuhgr2  35106  lfuhgr3  35107  acycgr1v  35136  umgracycusgr  35141  cusgracyclt3v  35143  dmopab3rexdif  35392  wzel  35812  dfrdg4  35939  bj-sbeq  36889  bj-sbel1  36893  bj-snsetex  36951  bj-snglc  36957  bj-taginv  36974  bj-adjfrombun  37034  poimirlem16  37630  poimirlem19  37633  eldmres  38259  ecres  38267  eldmqsres  38275  inxprnres  38280  cnvepres  38286  idinxpss  38300  inxpssidinxp  38304  idinxpssinxp  38305  cnvref5  38333  alrmomorn  38340  alrmomodm  38341  brxrn  38356  dfxrn2  38358  dmcnvep  38361  inxpxrn  38381  rnxrn  38384  rnxrnres  38385  rnxrncnvepres  38386  rnxrnidres  38387  coss1cnvres  38408  coss2cnvepres  38409  1cossres  38420  dfcoels  38421  refressn  38434  br1cossinidres  38440  br1cossincnvepres  38441  br1cossxrnidres  38442  br1cossxrncnvepres  38443  refrelcosslem  38453  coss0  38470  cossid  38471  br1cossxrncnvssrres  38499  dfrefrels2  38504  dfcnvrefrels2  38519  dfcnvrefrels3  38520  dfsymrels2  38536  dftrrels2  38566  eldmqs1cossres  38651  dfeldisj5  38713  disjres  38736  antisymrelres  38755  disjdmqsss  38794  disjdmqscossss  38795  mpets  38834  dmqsblocks  38845  prter2  38874  cdleme31sdnN  40381  evl1gprodd  42105  sn-iotalem  42209  inintabss  43567  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  comptiunov2i  43695  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  rr-grothprimbi  44284  rr-groth  44288  dfuniv2  44291  onfrALTlem4VD  44875  iinssiin  45123  iinssf  45132  iindif2f  45154  rnmptpr  45171  wessf1ornlem  45179  disjinfi  45186  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  ellimcabssub0  45615  eusnsn  47027  dfdfat2  47129  iineq0  48808  iinxp  48819  mofeu  48836  tposres0  48865  iinfsubc  49047  onsetreclem1  49694