Theorem elv 3435

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  csbconstg  3857  csbvarg  4375  iinconst  4945  iuniin  4947  iinssiun  4948  iinss1  4950  ssiinf  4998  iinss  5000  iinss2  5001  iinab  5011  iinun2  5016  iundif2  5017  iindif1  5018  iindif2  5020  iinin2  5021  iinpw  5049  brab1  5134  triin  5209  eusvnf  5327  sbcop  5435  iunopab  5505  pwvabrel  5673  ssrel  5730  xpiindi  5782  dmopab2rex  5864  dfima2  6019  args  6049  inisegn0  6055  dffr3  6056  dfse2  6057  cnv0  6095  dfco2a  6202  dfpo2  6252  iotaval2  6461  iinpreima  7013  tfinds2  7806  fvresex  7904  sbcoteq1a  7995  fnse  8074  xpord2pred  8086  xpord3lem  8090  xpord3pred  8093  suppvalbr  8105  cnvimadfsn  8113  reldmtpos  8175  rntpos  8180  ovtpos  8182  dftpos3  8185  tpostpos  8187  fprlem2  8242  onovuni  8273  oarec  8488  eqerlem  8670  elecreseq  8684  ixpiin  8863  ixpsnf1o  8877  boxriin  8879  idssen  8935  unxpdomlem3  9159  ac6sfi  9185  unbnn2  9198  fifo  9336  inf0  9531  ttrclselem2  9636  ttrclse  9637  rankxpsuc  9795  tcrank  9797  harcard  9891  infxpenlem  9924  infpwfien  9973  alephcard  9981  dfac3  10032  cflm  10161  fin23lem34  10257  dffin7-2  10309  fin1a2lem13  10323  itunitc1  10331  itunitc  10332  ituniiun  10333  hsmexlem4  10340  fin41  10355  axdclem2  10431  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  canthwe  10563  pwfseqlem5  10575  axgroth2  10737  axgroth6  10740  grothac  10742  grothtsk  10747  seqfeq4  14002  serle  14008  seqof  14010  hash1snb  14370  hashmap  14386  hashfun  14388  hashbclem  14403  hashf1lem2  14407  hashf1  14408  hash2prde  14421  prprrab  14424  hash3tpexb  14445  fi1uzind  14458  brfi1indALT  14461  s3sndisj  14918  s3iunsndisj  14919  rexfiuz  15299  fsumabs  15753  incexclem  15790  fprodcllemf  15912  fprodmodd  15951  iserodd  16795  hashbc0  16965  0ram  16980  ramub1  16988  initoid  17957  termoid  17958  equivestrcsetc  18107  gsumwspan  18803  gsmsymgrfix  19392  symgfixf1  19401  frgpnabllem1  19837  telgsums  19957  opprsubg  20321  subrngpropd  20534  subrgpropd  20574  coe1fzgsumdlem  22277  evl1gsumdlem  22330  mdetunilem9  22594  topnex  22970  neitr  23154  ordtbas2  23165  pnfnei  23194  mnfnei  23195  hauscmplem  23380  2ndcsb  23423  2ndcsep  23433  ptpjopn  23586  snfil  23838  fbasrn  23858  rnelfmlem  23926  rnelfm  23927  fmfnfmlem3  23930  fmfnfmlem4  23931  fmfnfm  23932  fclscmp  24004  alexsubALTlem4  24024  ptcmplem2  24027  symgtgp  24080  ustfilxp  24187  restutopopn  24212  ustuqtop2  24216  utopsnneiplem  24221  imasdsf1olem  24347  xpsdsval  24355  metuel2  24539  metustbl  24540  restmetu  24544  xrtgioo  24781  minveclem3b  25404  ovoliunlem1  25478  uniioombllem3  25561  itg1addlem4  25675  dvnff  25899  dvfsumlem3  26007  logfac  26581  gausslemma2dlem1a  27347  onsis  28285  ons2ind  28286  umgrislfupgrlem  29210  lfuhgr1v0e  29342  cplgrop  29525  finsumvtxdg2size  29639  rgrusgrprc  29678  elwspths2spth  30058  fusgr2wsp2nb  30424  h2hlm  31071  axhcompl-zf  31089  opsbc2ie  32565  inpr0  32622  iuninc  32650  disjpreima  32674  suppss2f  32731  fnpreimac  32763  tocyccntz  33225  elrgspnlem1  33323  elrgspnlem2  33324  nsgqusf1olem2  33494  nsgqusf1olem3  33495  zarclsiin  34036  esumpfinvalf  34241  measiuns  34382  bnj23  34882  bnj110  35021  bnj1123  35149  bnj1373  35193  fineqvnttrclse  35289  lfuhgr2  35322  lfuhgr3  35323  acycgr1v  35352  umgracycusgr  35357  cusgracyclt3v  35359  dmopab3rexdif  35608  wzel  36025  dfrdg4  36154  bj-sbeq  37221  bj-sbel1  37225  bj-snsetex  37283  bj-snglc  37289  bj-taginv  37306  bj-adjfrombun  37366  poimirlem16  37968  poimirlem19  37971  eldmres  38609  ecres  38617  eldmqsres  38625  inxprnres  38630  cnvepres  38636  idinxpss  38650  inxpssidinxp  38654  idinxpssinxp  38655  cnvref5  38683  alrmomorn  38690  alrmomodm  38691  ssdmral  38711  brxrn  38715  dfxrn2  38717  dmcnvep  38720  inxpxrn  38750  rnxrn  38753  rnxrnres  38754  rnxrncnvepres  38755  rnxrnidres  38756  blockadjliftmap  38790  dfsucmap3  38795  dmsucmap  38800  dfsuccl4  38806  coss1cnvres  38839  coss2cnvepres  38840  1cossres  38851  dfcoels  38852  refressn  38865  br1cossinidres  38871  br1cossincnvepres  38872  br1cossxrnidres  38873  br1cossxrncnvepres  38874  refrelcosslem  38884  coss0  38901  cossid  38902  br1cossxrncnvssrres  38920  dfrefrels2  38925  dfcnvrefrels2  38940  dfcnvrefrels3  38941  dfsymrels2  38957  dftrrels2  38991  eldmqs1cossres  39076  disjimdmqseq  39141  dfeldisj5  39145  eldisjdmqsim  39149  disjres  39176  antisymrelres  39198  disjdmqsss  39237  disjdmqscossss  39238  mpets  39288  dmqsblocks  39299  dfpeters2  39306  prter2  39338  cdleme31sdnN  40844  evl1gprodd  42567  sn-iotalem  42673  inintabss  44020  inintabd  44021  cnvcnvintabd  44042  cnvintabd  44045  comptiunov2i  44148  cotrcltrcl  44167  corcltrcl  44181  cotrclrcl  44184  rr-grothprimbi  44737  rr-groth  44741  dfuniv2  44744  onfrALTlem4VD  45327  iinssiin  45574  iinssf  45583  iindif2f  45605  rnmptpr  45622  wessf1ornlem  45630  disjinfi  45637  rnmptlb  45687  rnmptbddlem  45688  rnmptbd2lem  45692  ellimcabssub0  46062  preimageiingt  47163  preimaleiinlt  47164  eusnsn  47471  dfdfat2  47573  iineq0  49292  iinxp  49303  mofeu  49320  tposres0  49349  iinfsubc  49530  onsetreclem1  50177