Theorem elv 3428

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  csbconstg  3847  csbvarg  4362  dfopif  4797  iinconst  4931  iuniin  4933  iinssiun  4934  iinss1  4936  ssiinf  4980  iinss  4982  iinss2  4983  iinab  4993  iinun2  4998  iundif2  4999  iindif1  5000  iindif2  5002  iinin2  5003  iinpw  5031  brab1  5118  triin  5202  eusvnf  5310  sbcop  5397  pwvabrel  5629  difopab  5729  xpiindi  5733  dmopab2rex  5815  dfima2  5960  args  5989  inisegn0  5995  dffr3  5996  dfse2  5997  dfco2a  6139  dfpo2  6188  iotaval  6392  iinpreima  6928  tfinds2  7685  fvresex  7776  fnse  7945  suppvalbr  7952  cnvimadfsn  7959  reldmtpos  8021  rntpos  8026  ovtpos  8028  dftpos3  8031  tpostpos  8033  fprlem2  8088  wfrlem10OLD  8120  onovuni  8144  oarec  8355  eqerlem  8490  ixpiin  8670  ixpsnf1o  8684  boxriin  8686  idssen  8740  unxpdomlem3  8958  ac6sfi  8988  unbnn2  9001  fifo  9121  inf0  9309  rankxpsuc  9571  tcrank  9573  harcard  9667  infxpenlem  9700  infpwfien  9749  alephcard  9757  dfac3  9808  cflm  9937  fin23lem34  10033  dffin7-2  10085  fin1a2lem13  10099  itunitc1  10107  itunitc  10108  ituniiun  10109  hsmexlem4  10116  fin41  10131  axdclem2  10207  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  canthwe  10338  pwfseqlem5  10350  axgroth2  10512  axgroth6  10515  grothac  10517  grothtsk  10522  seqfeq4  13700  serle  13706  seqof  13708  hash1snb  14062  hashmap  14078  hashfun  14080  hashbclem  14092  hashf1lem2  14098  hashf1  14099  hash2prde  14112  prprrab  14115  fi1uzind  14139  brfi1indALT  14142  s3sndisj  14606  s3iunsndisj  14607  rexfiuz  14987  fsumabs  15441  incexclem  15476  fprodcllemf  15596  fprodmodd  15635  iserodd  16464  hashbc0  16634  0ram  16649  ramub1  16657  initoid  17632  termoid  17633  equivestrcsetc  17785  gsumwspan  18400  gsmsymgrfix  18951  symgfixf1  18960  frgpnabllem1  19389  telgsums  19509  opprsubg  19793  subrgpropd  19974  coe1fzgsumdlem  21382  evl1gsumdlem  21432  mdetunilem9  21677  topnex  22054  neitr  22239  ordtbas2  22250  pnfnei  22279  mnfnei  22280  hauscmplem  22465  2ndcsb  22508  2ndcsep  22518  ptpjopn  22671  snfil  22923  fbasrn  22943  rnelfmlem  23011  rnelfm  23012  fmfnfmlem3  23015  fmfnfmlem4  23016  fmfnfm  23017  fclscmp  23089  alexsubALTlem4  23109  ptcmplem2  23112  symgtgp  23165  ustfilxp  23272  restutopopn  23298  ustuqtop2  23302  utopsnneiplem  23307  imasdsf1olem  23434  xpsdsval  23442  metuel2  23627  metustbl  23628  restmetu  23632  xrtgioo  23875  minveclem3b  24497  ovoliunlem1  24571  uniioombllem3  24654  itg1addlem4  24768  itg1addlem4OLD  24769  dvnff  24992  dvfsumlem3  25097  logfac  25661  gausslemma2dlem1a  26418  umgrislfupgrlem  27395  lfuhgr1v0e  27524  cplgrop  27707  finsumvtxdg2size  27820  rgrusgrprc  27859  elwspths2spth  28233  fusgr2wsp2nb  28599  h2hlm  29243  axhcompl-zf  29261  opsbc2ie  30725  inpr0  30781  iuninc  30801  disjpreima  30824  suppss2f  30875  fnpreimac  30910  tocyccntz  31313  nsgqusf1olem2  31501  nsgqusf1olem3  31502  zarclsiin  31723  esumpfinvalf  31944  measiuns  32085  bnj23  32597  bnj110  32738  bnj1123  32866  bnj1373  32910  lfuhgr2  32980  lfuhgr3  32981  acycgr1v  33011  umgracycusgr  33016  cusgracyclt3v  33018  dmopab3rexdif  33267  ttrclselem2  33712  ttrclse  33713  xpord2pred  33719  xpord3pred  33725  wzel  33745  dfrdg4  34180  bj-sbeq  35013  bj-sbel1  35017  bj-snsetex  35080  bj-snglc  35086  bj-taginv  35103  poimirlem16  35720  poimirlem19  35723  eldmres  36335  ecres  36340  ecres2  36341  eldmqsres  36348  inxprnres  36354  cnvepres  36360  idinxpss  36375  inxpssidinxp  36378  idinxpssinxp  36379  alrmomorn  36417  alrmomodm  36418  brxrn  36431  dfxrn2  36433  inxpxrn  36448  rnxrn  36451  rnxrnres  36452  rnxrncnvepres  36453  rnxrnidres  36454  1cossres  36479  dfcoels  36480  br1cossinidres  36494  br1cossincnvepres  36495  br1cossxrnidres  36496  br1cossxrncnvepres  36497  refrelcosslem  36507  coss0  36524  cossid  36525  br1cossxrncnvssrres  36553  dfrefrels2  36558  dfcnvrefrels2  36571  dfcnvrefrels3  36572  dfsymrels2  36586  dftrrels2  36616  eldmqs1cossres  36698  dfeldisj5  36759  prter2  36822  cdleme31sdnN  38328  sn-iotalem  40117  sn-iotaval  40119  inintabss  41075  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  comptiunov2i  41203  cotrcltrcl  41222  corcltrcl  41236  cotrclrcl  41239  rr-grothprimbi  41802  rr-groth  41806  dfuniv2  41809  onfrALTlem4VD  42395  iinssiin  42567  iinssf  42576  rnmptpr  42602  wessf1ornlem  42611  disjinfi  42620  rnmptlb  42677  rnmptbddlem  42678  rnmptbd2lem  42683  ellimcabssub0  43048  eusnsn  44407  dfdfat2  44507  mofeu  46063  onsetreclem1  46296