Theorem elv 3468

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  csbconstg  3880  csbvarg  4405  iinconst  4971  iuniin  4973  iinssiun  4974  iinss1  4976  ssiinf  5023  iinss  5025  iinss2  5026  iinab  5036  iinun2  5041  iundif2  5042  iindif1  5045  iindif2  5047  iinin2  5048  iinpw  5076  brab1  5163  triin  5239  eusvnf  5364  sbcop  5472  iunopab  5545  pwvabrel  5713  ssrel  5770  xpiindi  5822  cnv0  5870  dmopab2rex  5908  dfima2  6065  args  6095  inisegn0  6101  dffr3  6102  dfse2  6103  dfco2a  6248  dfpo2  6298  iotaval2  6508  iinpreima  7065  tfinds2  7859  fvresex  7956  sbcoteq1a  8047  fnse  8128  xpord2pred  8140  xpord3lem  8144  xpord3pred  8147  suppvalbr  8159  cnvimadfsn  8167  reldmtpos  8229  rntpos  8234  ovtpos  8236  dftpos3  8239  tpostpos  8241  fprlem2  8297  onovuni  8328  oarec  8546  eqerlem  8729  elecreseq  8743  ixpiin  8921  ixpsnf1o  8935  boxriin  8937  idssen  8993  unxpdomlem3  9217  ac6sfi  9243  unbnn2  9256  fifo  9391  inf0  9589  ttrclselem2  9694  ttrclse  9695  rankxpsuc  9853  tcrank  9855  harcard  9963  infxpenlem  9996  infpwfien  10045  alephcard  10053  dfac3  10104  cflm  10232  fin23lem34  10329  dffin7-2  10381  fin1a2lem13  10395  itunitc1  10403  itunitc  10404  ituniiun  10405  hsmexlem4  10412  fin41  10427  axdclem2  10503  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  canthwe  10635  pwfseqlem5  10647  axgroth2  10809  axgroth6  10812  grothac  10814  grothtsk  10819  seqfeq4  14086  serle  14092  seqof  14094  hash1snb  14455  hashmap  14471  hashfun  14473  hashbclem  14488  hashf1lem2  14492  hashf1  14493  hash2prde  14506  prprrab  14509  hash3tpexb  14530  fi1uzind  14543  brfi1indALT  14546  s3sndisj  15003  s3iunsndisj  15004  rexfiuz  15398  fsumabs  15852  incexclem  15889  fprodcllemf  16011  fprodmodd  16050  iserodd  16894  hashbc0  17064  0ram  17079  ramub1  17087  initoid  18057  termoid  18058  equivestrcsetc  18207  gsumwspan  18904  gsmsymgrfix  19497  symgfixf1  19506  frgpnabllem1  19942  telgsums  20062  opprsubg  20433  subrngpropd  20652  subrgpropd  20692  coe1fzgsumdlem  22431  evl1gsumdlem  22484  mdetunilem9  22745  topnex  23121  neitr  23305  ordtbas2  23316  pnfnei  23345  mnfnei  23346  hauscmplem  23531  2ndcsb  23574  2ndcsep  23584  ptpjopn  23737  snfil  23989  fbasrn  24009  rnelfmlem  24077  rnelfm  24078  fmfnfmlem3  24081  fmfnfmlem4  24082  fmfnfm  24083  fclscmp  24155  alexsubALTlem4  24175  ptcmplem2  24178  symgtgp  24231  ustfilxp  24338  restutopopn  24363  ustuqtop2  24367  utopsnneiplem  24372  imasdsf1olem  24498  xpsdsval  24506  metuel2  24690  metustbl  24691  restmetu  24695  xrtgioo  24932  minveclem3b  25555  ovoliunlem1  25629  uniioombllem3  25712  itg1addlem4  25826  dvnff  26050  dvfsumlem3  26155  logfac  26731  gausslemma2dlem1a  27494  onsis  28432  ons2ind  28433  umgrislfupgrlem  29412  lfuhgr1v0e  29544  cplgrop  29727  finsumvtxdg2size  29840  rgrusgrprc  29879  elwspths2spth  30259  fusgr2wsp2nb  30625  h2hlm  31272  axhcompl-zf  31290  opsbc2ie  32762  inpr0  32818  iuninc  32845  disjpreima  32869  suppss2f  32923  fnpreimac  32955  tocyccntz  33404  elrgspnlem1  33502  elrgspnlem2  33503  nsgqusf1olem2  33666  nsgqusf1olem3  33667  zarclsiin  34205  esumpfinvalf  34410  measiuns  34551  bnj23  35051  bnj110  35190  bnj1123  35318  bnj1373  35362  fineqvnttrclse  35459  lfuhgr2  35509  lfuhgr3  35510  acycgr1v  35539  umgracycusgr  35544  cusgracyclt3v  35546  dmopab3rexdif  35795  wzel  36212  dfrdg4  36341  bj-sbeq  37424  bj-sbel1  37428  bj-snsetex  37486  bj-snglc  37492  bj-taginv  37509  bj-adjfrombun  37569  poimirlem16  38174  poimirlem19  38177  eldmres  38815  ecres  38823  eldmqsres  38831  inxprnres  38836  cnvepres  38842  idinxpss  38856  inxpssidinxp  38860  idinxpssinxp  38861  cnvref5  38889  alrmomorn  38896  alrmomodm  38897  ssdmral  38917  brxrn  38921  dfxrn2  38923  dmcnvep  38926  inxpxrn  38956  rnxrn  38959  rnxrnres  38960  rnxrncnvepres  38961  rnxrnidres  38962  blockadjliftmap  38996  dfsucmap3  39001  dmsucmap  39006  dfsuccl4  39012  coss1cnvres  39045  coss2cnvepres  39046  1cossres  39057  dfcoels  39058  refressn  39071  br1cossinidres  39077  br1cossincnvepres  39078  br1cossxrnidres  39079  br1cossxrncnvepres  39080  refrelcosslem  39090  coss0  39107  cossid  39108  br1cossxrncnvssrres  39126  dfrefrels2  39131  dfcnvrefrels2  39146  dfcnvrefrels3  39147  dfsymrels2  39163  dftrrels2  39197  eldmqs1cossres  39282  disjimdmqseq  39347  dfeldisj5  39351  eldisjdmqsim  39355  disjres  39382  antisymrelres  39404  disjdmqsss  39443  disjdmqscossss  39444  mpets  39494  dmqsblocks  39505  dfpeters2  39512  prter2  39544  cdleme31sdnN  41050  evl1gprodd  42773  sn-iotalem  42881  inintabss  44195  inintabd  44196  cnvcnvintabd  44217  cnvintabd  44220  comptiunov2i  44323  cotrcltrcl  44342  corcltrcl  44356  cotrclrcl  44359  rr-grothprimbi  44896  rr-groth  44900  dfuniv2  44903  onfrALTlem4VD  45485  iinssiin  45738  iinssf  45747  iindif2f  45769  rnmptpr  45786  wessf1ornlem  45794  disjinfi  45801  rnmptlb  45849  rnmptbddlem  45850  rnmptbd2lem  45854  ellimcabssub0  46224  preimageiingt  47325  preimaleiinlt  47326  eusnsn  47651  dfdfat2  47753  iineq0  49482  iinxp  49493  mofeu  49510  tposres0  49539  iinfsubc  49720  onsetreclem1  50367