Theorem elv 3462

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  csbconstg  3873  csbvarg  4399  iinconst  4969  iuniin  4971  iinssiun  4972  iinss1  4974  ssiinf  5021  iinss  5023  iinss2  5024  iinab  5034  iinun2  5039  iundif2  5040  iindif1  5043  iindif2  5045  iinin2  5046  iinpw  5074  brab1  5161  triin  5237  eusvnf  5365  sbcop  5473  iunopab  5546  pwvabrel  5714  ssrel  5771  xpiindi  5823  cnv0  5871  dmopab2rex  5909  dfima2  6066  args  6096  inisegn0  6102  dffr3  6103  dfse2  6104  dfco2a  6249  dfpo2  6301  iotaval2  6511  iinpreima  7068  tfinds2  7866  fvresex  7963  sbcoteq1a  8054  fnse  8135  xpord2pred  8147  xpord3lem  8151  xpord3pred  8154  suppvalbr  8166  cnvimadfsn  8174  reldmtpos  8236  rntpos  8241  ovtpos  8243  dftpos3  8246  tpostpos  8248  fprlem2  8304  onovuni  8335  oarec  8553  eqerlem  8736  elecreseq  8750  ixpiin  8928  ixpsnf1o  8942  boxriin  8944  idssen  9000  unxpdomlem3  9225  ac6sfi  9251  unbnn2  9264  fifo  9399  inf0  9597  ttrclselem2  9702  ttrclse  9703  rankxpsuc  9861  tcrank  9863  harcard  9980  infxpenlem  10013  infpwfien  10062  alephcard  10070  dfac3  10121  cflm  10248  fin23lem34  10345  dffin7-2  10397  fin1a2lem13  10411  itunitc1  10419  itunitc  10420  ituniiun  10421  hsmexlem4  10428  fin41  10443  axdclem2  10519  fpwwe2lem11  10643  fpwwe2lem12  10644  fpwwe2  10645  canthwe  10653  pwfseqlem5  10665  axgroth2  10827  axgroth6  10830  grothac  10832  grothtsk  10837  seqfeq4  14107  serle  14113  seqof  14115  hash1snb  14476  hashmap  14492  hashfun  14494  hashbclem  14509  hashf1lem2  14513  hashf1  14514  hash2prde  14527  prprrab  14530  hash3tpexb  14551  fi1uzind  14564  brfi1indALT  14567  s3sndisj  15030  s3iunsndisj  15031  rexfiuz  15425  fsumabs  15878  incexclem  15915  fprodcllemf  16037  fprodmodd  16076  iserodd  16919  hashbc0  17089  0ram  17104  ramub1  17112  initoid  18082  termoid  18083  equivestrcsetc  18232  gsumwspan  18944  gsmsymgrfix  19544  symgfixf1  19553  frgpnabllem1  19989  telgsums  20109  opprsubg  20482  subrngpropd  20719  subrgpropd  20759  coe1fzgsumdlem  22515  evl1gsumdlem  22568  mdetunilem9  22829  topnex  23205  neitr  23389  ordtbas2  23400  pnfnei  23429  mnfnei  23430  hauscmplem  23615  2ndcsb  23658  2ndcsep  23669  ptpjopn  23822  snfil  24074  fbasrn  24094  rnelfmlem  24162  rnelfm  24163  fmfnfmlem3  24166  fmfnfmlem4  24167  fmfnfm  24168  fclscmp  24240  alexsubALTlem4  24260  ptcmplem2  24263  symgtgp  24316  ustfilxp  24423  restutopopn  24448  ustuqtop2  24452  utopsnneiplem  24457  imasdsf1olem  24583  xpsdsval  24591  metuel2  24775  metustbl  24776  restmetu  24780  xrtgioo  25017  minveclem3b  25640  ovoliunlem1  25714  uniioombllem3  25797  itg1addlem4  25911  dvnff  26135  dvfsumlem3  26240  logfac  26819  gausslemma2dlem1a  27582  onsis  28520  ons2ind  28521  umgrislfupgrlem  29529  lfuhgr2  29556  lfuhgr3  29557  lfuhgr1v0e  29664  cplgrop  29847  finsumvtxdg2size  29960  rgrusgrprc  29999  elwspths2spth  30388  fusgr2wsp2nb  30758  h2hlm  31405  axhcompl-zf  31423  opsbc2ie  32895  inpr0  32951  iuninc  32978  disjpreima  33002  suppss2f  33056  fnpreimac  33088  tocyccntz  33530  elrgspnlem1  33628  elrgspnlem2  33629  nsgqusf1olem2  33789  nsgqusf1olem3  33790  zarclsiin  34327  esumpfinvalf  34532  measiuns  34674  bnj23  35174  bnj110  35313  bnj1123  35441  bnj1373  35485  fineqvnttrclse  35596  kardeq0  35628  acycgr1v  35680  umgracycusgr  35685  cusgracyclt3v  35687  dmopab3rexdif  35936  wzel  36353  dfrdg4  36482  bj-sbeq  37595  bj-sbel1  37599  bj-snsetex  37658  bj-snglc  37664  bj-taginv  37681  bj-adjfrombun  37741  poimirlem16  38346  poimirlem19  38349  findcard4  38424  eldmres  38986  ecres  38994  eldmqsres  39002  inxprnres  39007  cnvepres  39013  idinxpss  39027  inxpssidinxp  39031  idinxpssinxp  39032  cnvref5  39060  alrmomorn  39067  alrmomodm  39068  ssdmral  39088  brxrn  39092  dfxrn2  39094  dmcnvep  39097  inxpxrn  39127  rnxrn  39130  rnxrnres  39131  rnxrncnvepres  39132  rnxrnidres  39133  blockadjliftmap  39167  dfsucmap3  39172  dmsucmap  39177  dfsuccl4  39183  coss1cnvres  39216  coss2cnvepres  39217  1cossres  39228  dfcoels  39229  refressn  39242  br1cossinidres  39248  br1cossincnvepres  39249  br1cossxrnidres  39250  br1cossxrncnvepres  39251  refrelcosslem  39261  coss0  39278  cossid  39279  br1cossxrncnvssrres  39297  dfrefrels2  39302  dfcnvrefrels2  39317  dfcnvrefrels3  39318  dfsymrels2  39334  dftrrels2  39368  eldmqs1cossres  39453  disjimdmqseq  39518  dfeldisj5  39522  eldisjdmqsim  39526  disjres  39553  antisymrelres  39575  disjdmqsss  39614  disjdmqscossss  39615  mpets  39665  dmqsblocks  39676  dfpeters2  39683  prter2  39715  cdleme31sdnN  41221  evl1gprodd  42944  sn-iotalem  43052  inintabss  44364  inintabd  44365  cnvcnvintabd  44386  cnvintabd  44389  comptiunov2i  44492  cotrcltrcl  44511  corcltrcl  44525  cotrclrcl  44528  rr-grothprimbi  45065  rr-groth  45069  dfuniv2  45072  onfrALTlem4VD  45654  iinssiin  45907  iinssf  45916  iindif2f  45938  rnmptpr  45955  wessf1ornlem  45963  disjinfi  45970  rnmptlb  46018  rnmptbddlem  46019  rnmptbd2lem  46023  ellimcabssub0  46393  preimageiingt  47494  preimaleiinlt  47495  eusnsn  47823  dfdfat2  47925  iineq0  49657  iinxp  49668  mofeu  49685  tposres0  49714  iinfsubc  49895  onsetreclem1  50542