Theorem elv 3449

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446

This theorem is referenced by:  csbconstg  3878  csbvarg  4393  iinconst  4962  iuniin  4964  iinssiun  4965  iinss1  4967  ssiinf  5013  iinss  5015  iinss2  5016  iinab  5027  iinun2  5032  iundif2  5033  iindif1  5034  iindif2  5036  iinin2  5037  iinpw  5065  brab1  5150  triin  5226  eusvnf  5342  sbcop  5444  iunopab  5514  pwvabrel  5682  ssrel  5737  xpiindi  5789  dmopab2rex  5871  dfima2  6022  args  6052  inisegn0  6058  dffr3  6059  dfse2  6060  dfco2a  6207  dfpo2  6257  iotaval2  6467  iotavalOLD  6473  iinpreima  7023  tfinds2  7820  fvresex  7918  sbcoteq1a  8009  fnse  8089  xpord2pred  8101  xpord3lem  8105  xpord3pred  8108  suppvalbr  8120  cnvimadfsn  8128  reldmtpos  8190  rntpos  8195  ovtpos  8197  dftpos3  8200  tpostpos  8202  fprlem2  8257  onovuni  8288  oarec  8503  eqerlem  8683  elecreseq  8697  ixpiin  8874  ixpsnf1o  8888  boxriin  8890  idssen  8945  unxpdomlem3  9175  ac6sfi  9207  unbnn2  9220  fifo  9359  inf0  9550  ttrclselem2  9655  ttrclse  9656  rankxpsuc  9811  tcrank  9813  harcard  9907  infxpenlem  9942  infpwfien  9991  alephcard  9999  dfac3  10050  cflm  10179  fin23lem34  10275  dffin7-2  10327  fin1a2lem13  10341  itunitc1  10349  itunitc  10350  ituniiun  10351  hsmexlem4  10358  fin41  10373  axdclem2  10449  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  canthwe  10580  pwfseqlem5  10592  axgroth2  10754  axgroth6  10757  grothac  10759  grothtsk  10764  seqfeq4  13992  serle  13998  seqof  14000  hash1snb  14360  hashmap  14376  hashfun  14378  hashbclem  14393  hashf1lem2  14397  hashf1  14398  hash2prde  14411  prprrab  14414  hash3tpexb  14435  fi1uzind  14448  brfi1indALT  14451  s3sndisj  14909  s3iunsndisj  14910  rexfiuz  15290  fsumabs  15743  incexclem  15778  fprodcllemf  15900  fprodmodd  15939  iserodd  16782  hashbc0  16952  0ram  16967  ramub1  16975  initoid  17943  termoid  17944  equivestrcsetc  18093  gsumwspan  18755  gsmsymgrfix  19342  symgfixf1  19351  frgpnabllem1  19787  telgsums  19907  opprsubg  20272  subrngpropd  20488  subrgpropd  20528  coe1fzgsumdlem  22223  evl1gsumdlem  22276  mdetunilem9  22540  topnex  22916  neitr  23100  ordtbas2  23111  pnfnei  23140  mnfnei  23141  hauscmplem  23326  2ndcsb  23369  2ndcsep  23379  ptpjopn  23532  snfil  23784  fbasrn  23804  rnelfmlem  23872  rnelfm  23873  fmfnfmlem3  23876  fmfnfmlem4  23877  fmfnfm  23878  fclscmp  23950  alexsubALTlem4  23970  ptcmplem2  23973  symgtgp  24026  ustfilxp  24133  restutopopn  24159  ustuqtop2  24163  utopsnneiplem  24168  imasdsf1olem  24294  xpsdsval  24302  metuel2  24486  metustbl  24487  restmetu  24491  xrtgioo  24728  minveclem3b  25361  ovoliunlem1  25436  uniioombllem3  25519  itg1addlem4  25633  dvnff  25858  dvfsumlem3  25968  logfac  26543  gausslemma2dlem1a  27309  onsis  28212  umgrislfupgrlem  29102  lfuhgr1v0e  29234  cplgrop  29417  finsumvtxdg2size  29531  rgrusgrprc  29570  elwspths2spth  29947  fusgr2wsp2nb  30313  h2hlm  30959  axhcompl-zf  30977  opsbc2ie  32455  inpr0  32511  iuninc  32539  disjpreima  32563  suppss2f  32612  fnpreimac  32645  tocyccntz  33116  elrgspnlem1  33209  elrgspnlem2  33210  nsgqusf1olem2  33378  nsgqusf1olem3  33379  zarclsiin  33854  esumpfinvalf  34059  measiuns  34200  bnj23  34701  bnj110  34841  bnj1123  34969  bnj1373  35013  lfuhgr2  35099  lfuhgr3  35100  acycgr1v  35129  umgracycusgr  35134  cusgracyclt3v  35136  dmopab3rexdif  35385  wzel  35805  dfrdg4  35932  bj-sbeq  36882  bj-sbel1  36886  bj-snsetex  36944  bj-snglc  36950  bj-taginv  36967  bj-adjfrombun  37027  poimirlem16  37623  poimirlem19  37626  eldmres  38252  ecres  38260  eldmqsres  38268  inxprnres  38273  cnvepres  38279  idinxpss  38293  inxpssidinxp  38297  idinxpssinxp  38298  cnvref5  38326  alrmomorn  38333  alrmomodm  38334  brxrn  38349  dfxrn2  38351  dmcnvep  38354  inxpxrn  38374  rnxrn  38377  rnxrnres  38378  rnxrncnvepres  38379  rnxrnidres  38380  coss1cnvres  38401  coss2cnvepres  38402  1cossres  38413  dfcoels  38414  refressn  38427  br1cossinidres  38433  br1cossincnvepres  38434  br1cossxrnidres  38435  br1cossxrncnvepres  38436  refrelcosslem  38446  coss0  38463  cossid  38464  br1cossxrncnvssrres  38492  dfrefrels2  38497  dfcnvrefrels2  38512  dfcnvrefrels3  38513  dfsymrels2  38529  dftrrels2  38559  eldmqs1cossres  38644  dfeldisj5  38706  disjres  38729  antisymrelres  38748  disjdmqsss  38787  disjdmqscossss  38788  mpets  38827  dmqsblocks  38838  prter2  38867  cdleme31sdnN  40374  evl1gprodd  42098  sn-iotalem  42202  inintabss  43560  inintabd  43561  cnvcnvintabd  43582  cnvintabd  43585  comptiunov2i  43688  cotrcltrcl  43707  corcltrcl  43721  cotrclrcl  43724  rr-grothprimbi  44277  rr-groth  44281  dfuniv2  44284  onfrALTlem4VD  44868  iinssiin  45116  iinssf  45125  iindif2f  45147  rnmptpr  45164  wessf1ornlem  45172  disjinfi  45179  rnmptlb  45230  rnmptbddlem  45231  rnmptbd2lem  45235  ellimcabssub0  45608  eusnsn  47020  dfdfat2  47122  iineq0  48801  iinxp  48812  mofeu  48829  tposres0  48858  iinfsubc  49040  onsetreclem1  49687