Theorem elv 3456

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  csbconstg  3866  csbvarg  4392  iinconst  4962  iuniin  4964  iinssiun  4965  iinss1  4967  ssiinf  5013  iinss  5015  iinss2  5016  iinab  5026  iinun2  5031  iundif2  5032  iindif1  5035  iindif2  5037  iinin2  5038  iinpw  5066  brab1  5153  triin  5229  eusvnf  5354  sbcop  5459  iunopab  5534  pwvabrel  5702  ssrel  5759  xpiindi  5812  cnv0  5861  dmopab2rex  5899  dfima2  6058  args  6090  inisegn0  6096  dffr3  6097  dfse2  6098  dfco2a  6247  dfpo2  6299  iotaval2  6509  iinpreima  7069  tfinds2  7875  fvresex  7972  sbcoteq1a  8062  fnse  8150  xpord2pred  8162  xpord3lem  8166  xpord3pred  8169  suppvalbr  8181  cnvimadfsn  8189  reldmtpos  8251  rntpos  8256  ovtpos  8258  dftpos3  8261  tpostpos  8263  fprlem2  8319  onovuni  8350  oarec  8570  eqerlem  8753  elecreseq  8767  ixpiin  8952  ixpsnf1o  8966  boxriin  8968  idssen  9024  unxpdomlem3  9249  ac6sfi  9275  unbnn2  9289  fifo  9424  inf0  9622  ttrclselem2  9727  ttrclse  9728  rankxpsuc  9899  tcrank  9901  harcard  10059  infxpenlem  10092  infpwfien  10141  alephcard  10149  dfac3  10200  cflm  10327  fin23lem34  10424  dffin7-2  10476  fin1a2lem13  10490  itunitc1  10498  itunitc  10499  ituniiun  10500  hsmexlem4  10507  fin41  10522  axdclem2  10598  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  canthwe  10736  pwfseqlem5  10748  axgroth2  10910  axgroth6  10913  grothac  10915  grothtsk  10920  seqfeq4  14194  serle  14200  seqof  14202  hash1snb  14564  hashmap  14580  hashfun  14582  hashbclem  14597  hashf1lem2  14601  hashf1  14602  hash2prde  14615  prprrab  14618  hash3tpexb  14639  fi1uzind  14652  brfi1indALT  14655  s3sndisj  15120  s3iunsndisj  15121  rexfiuz  15515  fsumabs  15968  incexclem  16005  fprodcllemf  16125  fprodmodd  16164  iserodd  17013  hashbc0  17183  0ram  17198  ramub1  17206  initoid  18176  termoid  18177  equivestrcsetc  18326  gsumwspan  19042  gsmsymgrfix  19642  symgfixf1  19651  frgpnabllem1  20087  telgsums  20207  opprsubg  20582  subrngpropd  20820  subrgpropd  20860  coe1fzgsumdlem  22621  evl1gsumdlem  22674  mdetunilem9  22935  topnex  23314  neitr  23498  ordtbas2  23509  pnfnei  23538  mnfnei  23539  hauscmplem  23724  2ndcsb  23767  2ndcsep  23778  ptpjopn  23931  snfil  24183  fbasrn  24203  rnelfmlem  24271  rnelfm  24272  fmfnfmlem3  24275  fmfnfmlem4  24276  fmfnfm  24277  fclscmp  24349  alexsubALTlem4  24369  ptcmplem2  24372  symgtgp  24425  ustfilxp  24532  restutopopn  24557  ustuqtop2  24561  utopsnneiplem  24566  imasdsf1olem  24692  xpsdsval  24700  metuel2  24884  metustbl  24885  restmetu  24889  xrtgioo  25126  minveclem3b  25749  ovoliunlem1  25823  uniioombllem3  25906  itg1addlem4  26020  dvnff  26243  dvfsumlem3  26348  logfac  26929  gausslemma2dlem1a  27692  onsis  28660  ons2ind  28661  umgrislfupgrlem  29700  lfuhgr2  29727  lfuhgr3  29728  lfuhgr1v0e  29835  cplgrop  30018  finsumvtxdg2size  30131  rgrusgrprc  30170  elwspths2spth  30559  fusgr2wsp2nb  30935  h2hlm  31582  axhcompl-zf  31600  opsbc2ie  33072  inpr0  33128  iuninc  33155  disjpreima  33178  suppss2f  33232  fnpreimac  33264  tocyccntz  33705  elrgspnlem1  33803  elrgspnlem2  33804  nsgqusf1olem2  33965  nsgqusf1olem3  33966  zarclsiin  34503  esumpfinvalf  34708  measiuns  34850  bnj23  35349  bnj110  35488  bnj1123  35616  bnj1373  35660  fineqvnttrclse  35792  kardeq0  35824  acycgr1v  35914  umgracycusgr  35919  cusgracyclt3v  35921  dmopab3rexdif  36170  wzel  36586  dfrdg4  36715  bj-sbeq  37813  bj-sbel1  37817  bj-snsetex  37876  bj-snglc  37882  bj-taginv  37899  bj-adjfrombun  37959  poimirlem16  38554  poimirlem19  38557  findcard4  38632  dfprop2  38646  eldmres  39209  ecres  39217  eldmqsres  39225  inxprnres  39230  cnvepres  39236  idinxpss  39250  inxpssidinxp  39254  idinxpssinxp  39255  cnvref5  39283  alrmomorn  39290  alrmomodm  39291  ssdmral  39311  brxrn  39315  dfxrn2  39317  dmcnvep  39320  inxpxrn  39350  rnxrn  39353  rnxrnres  39354  rnxrncnvepres  39355  rnxrnidres  39356  blockadjliftmap  39390  dfsucmap3  39395  dmsucmap  39400  dfsuccl4  39406  coss1cnvres  39439  coss2cnvepres  39440  1cossres  39451  dfcoels  39452  refressn  39465  br1cossinidres  39471  br1cossincnvepres  39472  br1cossxrnidres  39473  br1cossxrncnvepres  39474  refrelcosslem  39484  coss0  39501  cossid  39502  br1cossxrncnvssrres  39520  dfrefrels2  39525  dfcnvrefrels2  39540  dfcnvrefrels3  39541  dfsymrels2  39557  dftrrels2  39591  eldmqs1cossres  39676  disjimdmqseq  39741  dfeldisj5  39745  eldisjdmqsim  39749  disjres  39776  antisymrelres  39798  disjdmqsss  39837  disjdmqscossss  39838  mpets  39888  dmqsblocks  39899  dfpeters2  39906  prter2  39938  cdleme31sdnN  41444  evl1gprodd  43167  sn-iotalem  43275  inintabss  44578  inintabd  44579  cnvcnvintabd  44599  cnvintabd  44602  comptiunov2i  44705  cotrcltrcl  44724  corcltrcl  44738  cotrclrcl  44741  rr-grothprimbi  45278  rr-groth  45282  dfuniv2  45285  onfrALTlem4VD  45867  iinssiin  46143  iinssf  46152  iindif2f  46174  rnmptpr  46191  wessf1ornlem  46199  disjinfi  46206  rnmptlb  46254  rnmptbddlem  46255  rnmptbd2lem  46259  ellimcabssub0  46628  preimageiingt  47729  preimaleiinlt  47730  eusnsn  48095  dfdfat2  48197  iineq0  49929  iinxp  49940  mofeu  49957  tposres0  49984  iinfsubc  50165  onsetreclem1  50797