Theorem elv 3415

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411

This theorem is referenced by:  csbvarg  4331  dfopif  4760  iinconst  4896  iuniin  4898  iinssiun  4899  iinss1  4901  ssiinf  4946  iinss  4948  iinss2  4949  iinab  4959  iinun2  4964  iundif2  4965  iindif1  4966  iindif2  4968  iinin2  4969  iinpw  4997  brab1  5084  triin  5157  eusvnf  5265  sbcop  5352  pwvabrel  5577  difopab  5677  xpiindi  5681  dmopab2rex  5763  dfima2  5908  args  5934  inisegn0  5938  dffr3  5939  dfse2  5940  dfco2a  6081  iotaval  6314  iinpreima  6834  tfinds2  7583  fvresex  7671  fnse  7838  suppvalbr  7845  cnvimadfsn  7852  reldmtpos  7916  rntpos  7921  ovtpos  7923  dftpos3  7926  tpostpos  7928  wfrlem10  7980  onovuni  7995  oarec  8204  eqerlem  8339  ixpiin  8519  ixpsnf1o  8533  boxriin  8535  idssen  8585  unxpdomlem3  8775  ac6sfi  8808  unbnn2  8821  fifo  8942  inf0  9130  rankxpsuc  9357  tcrank  9359  harcard  9453  infxpenlem  9486  infpwfien  9535  alephcard  9543  dfac3  9594  cflm  9723  fin23lem34  9819  dffin7-2  9871  fin1a2lem13  9885  itunitc1  9893  itunitc  9894  ituniiun  9895  hsmexlem4  9902  fin41  9917  axdclem2  9993  fpwwe2lem11  10114  fpwwe2lem12  10115  fpwwe2  10116  canthwe  10124  pwfseqlem5  10136  axgroth2  10298  axgroth6  10301  grothac  10303  grothtsk  10308  seqfeq4  13482  serle  13488  seqof  13490  hash1snb  13843  hashmap  13859  hashfun  13861  hashbclem  13873  hashf1lem2  13879  hashf1  13880  hash2prde  13893  prprrab  13896  fi1uzind  13920  brfi1indALT  13923  s3sndisj  14387  s3iunsndisj  14388  rexfiuz  14768  fsumabs  15217  incexclem  15252  fprodcllemf  15373  fprodmodd  15412  iserodd  16240  hashbc0  16409  0ram  16424  ramub1  16432  initoid  17340  termoid  17341  equivestrcsetc  17481  gsumwspan  18090  gsmsymgrfix  18636  symgfixf1  18645  frgpnabllem1  19074  telgsums  19194  opprsubg  19470  subrgpropd  19651  coe1fzgsumdlem  21038  evl1gsumdlem  21088  mdetunilem9  21333  topnex  21709  neitr  21893  ordtbas2  21904  pnfnei  21933  mnfnei  21934  hauscmplem  22119  2ndcsb  22162  2ndcsep  22172  ptpjopn  22325  snfil  22577  fbasrn  22597  rnelfmlem  22665  rnelfm  22666  fmfnfmlem3  22669  fmfnfmlem4  22670  fmfnfm  22671  fclscmp  22743  alexsubALTlem4  22763  ptcmplem2  22766  symgtgp  22819  ustfilxp  22926  restutopopn  22952  ustuqtop2  22956  utopsnneiplem  22961  imasdsf1olem  23088  xpsdsval  23096  metuel2  23280  metustbl  23281  restmetu  23285  xrtgioo  23520  minveclem3b  24141  ovoliunlem1  24215  uniioombllem3  24298  itg1addlem4  24412  dvnff  24635  dvfsumlem3  24740  logfac  25304  gausslemma2dlem1a  26061  umgrislfupgrlem  27027  lfuhgr1v0e  27156  cplgrop  27339  finsumvtxdg2size  27452  rgrusgrprc  27491  elwspths2spth  27865  fusgr2wsp2nb  28231  h2hlm  28875  axhcompl-zf  28893  opsbc2ie  30358  inpr0  30415  iuninc  30435  disjpreima  30458  suppss2f  30509  fnpreimac  30544  tocyccntz  30949  nsgqusf1olem2  31132  nsgqusf1olem3  31133  zarclsiin  31354  esumpfinvalf  31575  measiuns  31716  bnj23  32228  bnj110  32370  bnj1123  32498  bnj1373  32542  lfuhgr2  32608  lfuhgr3  32609  acycgr1v  32639  umgracycusgr  32644  cusgracyclt3v  32646  dmopab3rexdif  32895  dfpo2  33250  xpord2pred  33359  xpord3pred  33365  wzel  33385  fprlem2  33412  dfrdg4  33836  bj-sbeq  34656  bj-sbel1  34660  bj-snsetex  34714  bj-snglc  34720  bj-taginv  34737  poimirlem16  35387  poimirlem19  35390  eldmres  36004  ecres  36009  ecres2  36010  eldmqsres  36017  inxprnres  36023  cnvepres  36029  idinxpss  36044  inxpssidinxp  36047  idinxpssinxp  36048  alrmomorn  36086  alrmomodm  36087  brxrn  36100  dfxrn2  36102  inxpxrn  36117  rnxrn  36120  rnxrnres  36121  rnxrncnvepres  36122  rnxrnidres  36123  1cossres  36148  dfcoels  36149  br1cossinidres  36163  br1cossincnvepres  36164  br1cossxrnidres  36165  br1cossxrncnvepres  36166  refrelcosslem  36176  coss0  36193  cossid  36194  br1cossxrncnvssrres  36222  dfrefrels2  36227  dfcnvrefrels2  36240  dfcnvrefrels3  36241  dfsymrels2  36255  dftrrels2  36285  eldmqs1cossres  36367  dfeldisj5  36428  prter2  36491  cdleme31sdnN  37997  inintabss  40686  inintabd  40687  cnvcnvintabd  40708  cnvintabd  40711  comptiunov2i  40815  cotrcltrcl  40834  corcltrcl  40848  cotrclrcl  40851  rr-grothprimbi  41411  rr-groth  41415  onfrALTlem4VD  42000  iinssiin  42172  iinssf  42181  rnmptpr  42207  wessf1ornlem  42216  disjinfi  42225  rnmptlb  42283  rnmptbddlem  42284  rnmptbd2lem  42289  ellimcabssub0  42660  eusnsn  44019  dfdfat2  44101  onsetreclem1  45719