Theorem elv 3447

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442

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 3444

This theorem is referenced by:  csbconstg  3870  csbvarg  4388  iinconst  4959  iuniin  4961  iinssiun  4962  iinss1  4964  ssiinf  5012  iinss  5014  iinss2  5015  iinab  5025  iinun2  5030  iundif2  5031  iindif1  5032  iindif2  5034  iinin2  5035  iinpw  5063  brab1  5148  triin  5223  eusvnf  5339  sbcop  5445  iunopab  5515  pwvabrel  5683  ssrel  5740  xpiindi  5792  dmopab2rex  5874  dfima2  6029  args  6059  inisegn0  6065  dffr3  6066  dfse2  6067  cnv0  6105  dfco2a  6212  dfpo2  6262  iotaval2  6471  iinpreima  7023  tfinds2  7816  fvresex  7914  sbcoteq1a  8005  fnse  8085  xpord2pred  8097  xpord3lem  8101  xpord3pred  8104  suppvalbr  8116  cnvimadfsn  8124  reldmtpos  8186  rntpos  8191  ovtpos  8193  dftpos3  8196  tpostpos  8198  fprlem2  8253  onovuni  8284  oarec  8499  eqerlem  8681  elecreseq  8695  ixpiin  8874  ixpsnf1o  8888  boxriin  8890  idssen  8946  unxpdomlem3  9170  ac6sfi  9196  unbnn2  9209  fifo  9347  inf0  9542  ttrclselem2  9647  ttrclse  9648  rankxpsuc  9806  tcrank  9808  harcard  9902  infxpenlem  9935  infpwfien  9984  alephcard  9992  dfac3  10043  cflm  10172  fin23lem34  10268  dffin7-2  10320  fin1a2lem13  10334  itunitc1  10342  itunitc  10343  ituniiun  10344  hsmexlem4  10351  fin41  10366  axdclem2  10442  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  canthwe  10574  pwfseqlem5  10586  axgroth2  10748  axgroth6  10751  grothac  10753  grothtsk  10758  seqfeq4  13986  serle  13992  seqof  13994  hash1snb  14354  hashmap  14370  hashfun  14372  hashbclem  14387  hashf1lem2  14391  hashf1  14392  hash2prde  14405  prprrab  14408  hash3tpexb  14429  fi1uzind  14442  brfi1indALT  14445  s3sndisj  14902  s3iunsndisj  14903  rexfiuz  15283  fsumabs  15736  incexclem  15771  fprodcllemf  15893  fprodmodd  15932  iserodd  16775  hashbc0  16945  0ram  16960  ramub1  16968  initoid  17937  termoid  17938  equivestrcsetc  18087  gsumwspan  18783  gsmsymgrfix  19369  symgfixf1  19378  frgpnabllem1  19814  telgsums  19934  opprsubg  20300  subrngpropd  20513  subrgpropd  20553  coe1fzgsumdlem  22259  evl1gsumdlem  22312  mdetunilem9  22576  topnex  22952  neitr  23136  ordtbas2  23147  pnfnei  23176  mnfnei  23177  hauscmplem  23362  2ndcsb  23405  2ndcsep  23415  ptpjopn  23568  snfil  23820  fbasrn  23840  rnelfmlem  23908  rnelfm  23909  fmfnfmlem3  23912  fmfnfmlem4  23913  fmfnfm  23914  fclscmp  23986  alexsubALTlem4  24006  ptcmplem2  24009  symgtgp  24062  ustfilxp  24169  restutopopn  24194  ustuqtop2  24198  utopsnneiplem  24203  imasdsf1olem  24329  xpsdsval  24337  metuel2  24521  metustbl  24522  restmetu  24526  xrtgioo  24763  minveclem3b  25396  ovoliunlem1  25471  uniioombllem3  25554  itg1addlem4  25668  dvnff  25893  dvfsumlem3  26003  logfac  26578  gausslemma2dlem1a  27344  onsis  28282  ons2ind  28283  umgrislfupgrlem  29207  lfuhgr1v0e  29339  cplgrop  29522  finsumvtxdg2size  29636  rgrusgrprc  29675  elwspths2spth  30055  fusgr2wsp2nb  30421  h2hlm  31068  axhcompl-zf  31086  opsbc2ie  32562  inpr0  32619  iuninc  32647  disjpreima  32671  suppss2f  32728  fnpreimac  32760  tocyccntz  33238  elrgspnlem1  33336  elrgspnlem2  33337  nsgqusf1olem2  33507  nsgqusf1olem3  33508  zarclsiin  34049  esumpfinvalf  34254  measiuns  34395  bnj23  34895  bnj110  35034  bnj1123  35162  bnj1373  35206  fineqvnttrclse  35302  lfuhgr2  35335  lfuhgr3  35336  acycgr1v  35365  umgracycusgr  35370  cusgracyclt3v  35372  dmopab3rexdif  35621  wzel  36038  dfrdg4  36167  bj-sbeq  37149  bj-sbel1  37153  bj-snsetex  37211  bj-snglc  37217  bj-taginv  37234  bj-adjfrombun  37294  poimirlem16  37887  poimirlem19  37890  eldmres  38528  ecres  38536  eldmqsres  38544  inxprnres  38549  cnvepres  38555  idinxpss  38569  inxpssidinxp  38573  idinxpssinxp  38574  cnvref5  38602  alrmomorn  38609  alrmomodm  38610  ssdmral  38630  brxrn  38634  dfxrn2  38636  dmcnvep  38639  inxpxrn  38669  rnxrn  38672  rnxrnres  38673  rnxrncnvepres  38674  rnxrnidres  38675  blockadjliftmap  38709  dfsucmap3  38714  dmsucmap  38719  dfsuccl4  38725  coss1cnvres  38758  coss2cnvepres  38759  1cossres  38770  dfcoels  38771  refressn  38784  br1cossinidres  38790  br1cossincnvepres  38791  br1cossxrnidres  38792  br1cossxrncnvepres  38793  refrelcosslem  38803  coss0  38820  cossid  38821  br1cossxrncnvssrres  38839  dfrefrels2  38844  dfcnvrefrels2  38859  dfcnvrefrels3  38860  dfsymrels2  38876  dftrrels2  38910  eldmqs1cossres  38995  disjimdmqseq  39060  dfeldisj5  39064  eldisjdmqsim  39068  disjres  39095  antisymrelres  39117  disjdmqsss  39156  disjdmqscossss  39157  mpets  39207  dmqsblocks  39218  dfpeters2  39225  prter2  39257  cdleme31sdnN  40763  evl1gprodd  42487  sn-iotalem  42593  inintabss  43934  inintabd  43935  cnvcnvintabd  43956  cnvintabd  43959  comptiunov2i  44062  cotrcltrcl  44081  corcltrcl  44095  cotrclrcl  44098  rr-grothprimbi  44651  rr-groth  44655  dfuniv2  44658  onfrALTlem4VD  45241  iinssiin  45488  iinssf  45497  iindif2f  45519  rnmptpr  45536  wessf1ornlem  45544  disjinfi  45551  rnmptlb  45601  rnmptbddlem  45602  rnmptbd2lem  45606  ellimcabssub0  45977  preimageiingt  47078  preimaleiinlt  47079  eusnsn  47386  dfdfat2  47488  iineq0  49179  iinxp  49190  mofeu  49207  tposres0  49236  iinfsubc  49417  onsetreclem1  50064