Theorem elv 3436

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  csbconstg  3850  csbvarg  4362  iinconst  4932  iuniin  4934  iinssiun  4935  iinss1  4937  ssiinf  4984  iinss  4986  iinss2  4987  iinab  4997  iinun2  5002  iundif2  5003  iindif1  5004  iindif2  5006  iinin2  5007  iinpw  5035  brab1  5120  triin  5196  eusvnf  5321  sbcop  5429  iunopab  5501  pwvabrel  5669  ssrel  5726  xpiindi  5777  dmopab2rex  5859  dfima2  6014  args  6044  inisegn0  6050  dffr3  6051  dfse2  6052  cnv0  6090  dfco2a  6197  dfpo2  6247  iotaval2  6456  iinpreima  7010  tfinds2  7804  fvresex  7902  sbcoteq1a  7993  fnse  8073  xpord2pred  8085  xpord3lem  8089  xpord3pred  8092  suppvalbr  8104  cnvimadfsn  8112  reldmtpos  8174  rntpos  8179  ovtpos  8181  dftpos3  8184  tpostpos  8186  fprlem2  8241  onovuni  8272  oarec  8487  eqerlem  8669  elecreseq  8683  ixpiin  8862  ixpsnf1o  8876  boxriin  8878  idssen  8934  unxpdomlem3  9158  ac6sfi  9184  unbnn2  9197  fifo  9335  inf0  9533  ttrclselem2  9638  ttrclse  9639  rankxpsuc  9797  tcrank  9799  harcard  9893  infxpenlem  9926  infpwfien  9975  alephcard  9983  dfac3  10034  cflm  10163  fin23lem34  10259  dffin7-2  10311  fin1a2lem13  10325  itunitc1  10333  itunitc  10334  ituniiun  10335  hsmexlem4  10342  fin41  10357  axdclem2  10433  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  canthwe  10565  pwfseqlem5  10577  axgroth2  10739  axgroth6  10742  grothac  10744  grothtsk  10749  seqfeq4  14004  serle  14010  seqof  14012  hash1snb  14372  hashmap  14388  hashfun  14390  hashbclem  14405  hashf1lem2  14409  hashf1  14410  hash2prde  14423  prprrab  14426  hash3tpexb  14447  fi1uzind  14460  brfi1indALT  14463  s3sndisj  14920  s3iunsndisj  14921  rexfiuz  15301  fsumabs  15755  incexclem  15792  fprodcllemf  15914  fprodmodd  15953  iserodd  16797  hashbc0  16967  0ram  16982  ramub1  16990  initoid  17959  termoid  17960  equivestrcsetc  18109  gsumwspan  18805  gsmsymgrfix  19394  symgfixf1  19403  frgpnabllem1  19839  telgsums  19959  opprsubg  20323  subrngpropd  20540  subrgpropd  20580  coe1fzgsumdlem  22289  evl1gsumdlem  22342  mdetunilem9  22603  topnex  22979  neitr  23163  ordtbas2  23174  pnfnei  23203  mnfnei  23204  hauscmplem  23389  2ndcsb  23432  2ndcsep  23442  ptpjopn  23595  snfil  23847  fbasrn  23867  rnelfmlem  23935  rnelfm  23936  fmfnfmlem3  23939  fmfnfmlem4  23940  fmfnfm  23941  fclscmp  24013  alexsubALTlem4  24033  ptcmplem2  24036  symgtgp  24089  ustfilxp  24196  restutopopn  24221  ustuqtop2  24225  utopsnneiplem  24230  imasdsf1olem  24356  xpsdsval  24364  metuel2  24548  metustbl  24549  restmetu  24553  xrtgioo  24790  minveclem3b  25413  ovoliunlem1  25487  uniioombllem3  25570  itg1addlem4  25684  dvnff  25908  dvfsumlem3  26013  logfac  26583  gausslemma2dlem1a  27346  onsis  28284  ons2ind  28285  umgrislfupgrlem  29209  lfuhgr1v0e  29341  cplgrop  29524  finsumvtxdg2size  29637  rgrusgrprc  29676  elwspths2spth  30056  fusgr2wsp2nb  30422  h2hlm  31069  axhcompl-zf  31087  opsbc2ie  32563  inpr0  32620  iuninc  32649  disjpreima  32673  suppss2f  32730  fnpreimac  32762  tocyccntz  33225  elrgspnlem1  33323  elrgspnlem2  33324  nsgqusf1olem2  33497  nsgqusf1olem3  33498  zarclsiin  34055  esumpfinvalf  34260  measiuns  34401  bnj23  34901  bnj110  35040  bnj1123  35168  bnj1373  35212  fineqvnttrclse  35305  lfuhgr2  35347  lfuhgr3  35348  acycgr1v  35377  umgracycusgr  35382  cusgracyclt3v  35384  dmopab3rexdif  35633  wzel  36050  dfrdg4  36179  bj-sbeq  37254  bj-sbel1  37258  bj-snsetex  37316  bj-snglc  37322  bj-taginv  37339  bj-adjfrombun  37399  poimirlem16  38003  poimirlem19  38006  eldmres  38644  ecres  38652  eldmqsres  38660  inxprnres  38665  cnvepres  38671  idinxpss  38685  inxpssidinxp  38689  idinxpssinxp  38690  cnvref5  38718  alrmomorn  38725  alrmomodm  38726  ssdmral  38746  brxrn  38750  dfxrn2  38752  dmcnvep  38755  inxpxrn  38785  rnxrn  38788  rnxrnres  38789  rnxrncnvepres  38790  rnxrnidres  38791  blockadjliftmap  38825  dfsucmap3  38830  dmsucmap  38835  dfsuccl4  38841  coss1cnvres  38874  coss2cnvepres  38875  1cossres  38886  dfcoels  38887  refressn  38900  br1cossinidres  38906  br1cossincnvepres  38907  br1cossxrnidres  38908  br1cossxrncnvepres  38909  refrelcosslem  38919  coss0  38936  cossid  38937  br1cossxrncnvssrres  38955  dfrefrels2  38960  dfcnvrefrels2  38975  dfcnvrefrels3  38976  dfsymrels2  38992  dftrrels2  39026  eldmqs1cossres  39111  disjimdmqseq  39176  dfeldisj5  39180  eldisjdmqsim  39184  disjres  39211  antisymrelres  39233  disjdmqsss  39272  disjdmqscossss  39273  mpets  39323  dmqsblocks  39334  dfpeters2  39341  prter2  39373  cdleme31sdnN  40879  evl1gprodd  42602  sn-iotalem  42708  inintabss  44022  inintabd  44023  cnvcnvintabd  44044  cnvintabd  44047  comptiunov2i  44150  cotrcltrcl  44169  corcltrcl  44183  cotrclrcl  44186  rr-grothprimbi  44739  rr-groth  44743  dfuniv2  44746  onfrALTlem4VD  45329  iinssiin  45576  iinssf  45585  iindif2f  45607  rnmptpr  45624  wessf1ornlem  45632  disjinfi  45639  rnmptlb  45687  rnmptbddlem  45688  rnmptbd2lem  45692  ellimcabssub0  46062  preimageiingt  47163  preimaleiinlt  47164  eusnsn  47489  dfdfat2  47591  iineq0  49310  iinxp  49321  mofeu  49338  tposres0  49367  iinfsubc  49548  onsetreclem1  50195