Theorem elv 3445

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  csbconstg  3868  csbvarg  4386  iinconst  4957  iuniin  4959  iinssiun  4960  iinss1  4962  ssiinf  5010  iinss  5012  iinss2  5013  iinab  5023  iinun2  5028  iundif2  5029  iindif1  5030  iindif2  5032  iinin2  5033  iinpw  5061  brab1  5146  triin  5221  eusvnf  5337  sbcop  5437  iunopab  5507  pwvabrel  5675  ssrel  5732  xpiindi  5784  dmopab2rex  5866  dfima2  6021  args  6051  inisegn0  6057  dffr3  6058  dfse2  6059  cnv0  6097  dfco2a  6204  dfpo2  6254  iotaval2  6463  iinpreima  7014  tfinds2  7806  fvresex  7904  sbcoteq1a  7995  fnse  8075  xpord2pred  8087  xpord3lem  8091  xpord3pred  8094  suppvalbr  8106  cnvimadfsn  8114  reldmtpos  8176  rntpos  8181  ovtpos  8183  dftpos3  8186  tpostpos  8188  fprlem2  8243  onovuni  8274  oarec  8489  eqerlem  8670  elecreseq  8684  ixpiin  8862  ixpsnf1o  8876  boxriin  8878  idssen  8934  unxpdomlem3  9158  ac6sfi  9184  unbnn2  9197  fifo  9335  inf0  9530  ttrclselem2  9635  ttrclse  9636  rankxpsuc  9794  tcrank  9796  harcard  9890  infxpenlem  9923  infpwfien  9972  alephcard  9980  dfac3  10031  cflm  10160  fin23lem34  10256  dffin7-2  10308  fin1a2lem13  10322  itunitc1  10330  itunitc  10331  ituniiun  10332  hsmexlem4  10339  fin41  10354  axdclem2  10430  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  canthwe  10562  pwfseqlem5  10574  axgroth2  10736  axgroth6  10739  grothac  10741  grothtsk  10746  seqfeq4  13974  serle  13980  seqof  13982  hash1snb  14342  hashmap  14358  hashfun  14360  hashbclem  14375  hashf1lem2  14379  hashf1  14380  hash2prde  14393  prprrab  14396  hash3tpexb  14417  fi1uzind  14430  brfi1indALT  14433  s3sndisj  14890  s3iunsndisj  14891  rexfiuz  15271  fsumabs  15724  incexclem  15759  fprodcllemf  15881  fprodmodd  15920  iserodd  16763  hashbc0  16933  0ram  16948  ramub1  16956  initoid  17925  termoid  17926  equivestrcsetc  18075  gsumwspan  18771  gsmsymgrfix  19357  symgfixf1  19366  frgpnabllem1  19802  telgsums  19922  opprsubg  20288  subrngpropd  20501  subrgpropd  20541  coe1fzgsumdlem  22247  evl1gsumdlem  22300  mdetunilem9  22564  topnex  22940  neitr  23124  ordtbas2  23135  pnfnei  23164  mnfnei  23165  hauscmplem  23350  2ndcsb  23393  2ndcsep  23403  ptpjopn  23556  snfil  23808  fbasrn  23828  rnelfmlem  23896  rnelfm  23897  fmfnfmlem3  23900  fmfnfmlem4  23901  fmfnfm  23902  fclscmp  23974  alexsubALTlem4  23994  ptcmplem2  23997  symgtgp  24050  ustfilxp  24157  restutopopn  24182  ustuqtop2  24186  utopsnneiplem  24191  imasdsf1olem  24317  xpsdsval  24325  metuel2  24509  metustbl  24510  restmetu  24514  xrtgioo  24751  minveclem3b  25384  ovoliunlem1  25459  uniioombllem3  25542  itg1addlem4  25656  dvnff  25881  dvfsumlem3  25991  logfac  26566  gausslemma2dlem1a  27332  onsis  28270  ons2ind  28271  umgrislfupgrlem  29195  lfuhgr1v0e  29327  cplgrop  29510  finsumvtxdg2size  29624  rgrusgrprc  29663  elwspths2spth  30043  fusgr2wsp2nb  30409  h2hlm  31055  axhcompl-zf  31073  opsbc2ie  32550  inpr0  32607  iuninc  32635  disjpreima  32659  suppss2f  32716  fnpreimac  32749  tocyccntz  33226  elrgspnlem1  33324  elrgspnlem2  33325  nsgqusf1olem2  33495  nsgqusf1olem3  33496  zarclsiin  34028  esumpfinvalf  34233  measiuns  34374  bnj23  34874  bnj110  35014  bnj1123  35142  bnj1373  35186  fineqvnttrclse  35280  lfuhgr2  35313  lfuhgr3  35314  acycgr1v  35343  umgracycusgr  35348  cusgracyclt3v  35350  dmopab3rexdif  35599  wzel  36016  dfrdg4  36145  bj-sbeq  37102  bj-sbel1  37106  bj-snsetex  37164  bj-snglc  37170  bj-taginv  37187  bj-adjfrombun  37247  poimirlem16  37837  poimirlem19  37840  eldmres  38470  ecres  38478  eldmqsres  38486  inxprnres  38491  cnvepres  38497  idinxpss  38511  inxpssidinxp  38515  idinxpssinxp  38516  cnvref5  38544  alrmomorn  38551  alrmomodm  38552  ssdmral  38564  brxrn  38568  dfxrn2  38570  dmcnvep  38573  inxpxrn  38603  rnxrn  38606  rnxrnres  38607  rnxrncnvepres  38608  rnxrnidres  38609  blockadjliftmap  38633  dfsucmap3  38637  dmsucmap  38642  dfsuccl4  38648  coss1cnvres  38680  coss2cnvepres  38681  1cossres  38692  dfcoels  38693  refressn  38706  br1cossinidres  38712  br1cossincnvepres  38713  br1cossxrnidres  38714  br1cossxrncnvepres  38715  refrelcosslem  38725  coss0  38742  cossid  38743  br1cossxrncnvssrres  38761  dfrefrels2  38766  dfcnvrefrels2  38781  dfcnvrefrels3  38782  dfsymrels2  38798  dftrrels2  38832  eldmqs1cossres  38918  dfeldisj5  38980  disjres  39003  antisymrelres  39022  disjdmqsss  39061  disjdmqscossss  39062  mpets  39101  dmqsblocks  39112  prter2  39141  cdleme31sdnN  40647  evl1gprodd  42371  sn-iotalem  42477  inintabss  43819  inintabd  43820  cnvcnvintabd  43841  cnvintabd  43844  comptiunov2i  43947  cotrcltrcl  43966  corcltrcl  43980  cotrclrcl  43983  rr-grothprimbi  44536  rr-groth  44540  dfuniv2  44543  onfrALTlem4VD  45126  iinssiin  45373  iinssf  45382  iindif2f  45404  rnmptpr  45421  wessf1ornlem  45429  disjinfi  45436  rnmptlb  45487  rnmptbddlem  45488  rnmptbd2lem  45492  ellimcabssub0  45863  preimageiingt  46964  preimaleiinlt  46965  eusnsn  47272  dfdfat2  47374  iineq0  49065  iinxp  49076  mofeu  49093  tposres0  49122  iinfsubc  49303  onsetreclem1  49950