Theorem elv 3443

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440

This theorem is referenced by:  csbconstg  3866  csbvarg  4384  iinconst  4955  iuniin  4957  iinssiun  4958  iinss1  4960  ssiinf  5008  iinss  5010  iinss2  5011  iinab  5021  iinun2  5026  iundif2  5027  iindif1  5028  iindif2  5030  iinin2  5031  iinpw  5059  brab1  5144  triin  5219  eusvnf  5335  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  7012  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  8668  elecreseq  8682  ixpiin  8860  ixpsnf1o  8874  boxriin  8876  idssen  8932  unxpdomlem3  9156  ac6sfi  9182  unbnn2  9195  fifo  9333  inf0  9528  ttrclselem2  9633  ttrclse  9634  rankxpsuc  9792  tcrank  9794  harcard  9888  infxpenlem  9921  infpwfien  9970  alephcard  9978  dfac3  10029  cflm  10158  fin23lem34  10254  dffin7-2  10306  fin1a2lem13  10320  itunitc1  10328  itunitc  10329  ituniiun  10330  hsmexlem4  10337  fin41  10352  axdclem2  10428  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe2  10552  canthwe  10560  pwfseqlem5  10572  axgroth2  10734  axgroth6  10737  grothac  10739  grothtsk  10744  seqfeq4  13972  serle  13978  seqof  13980  hash1snb  14340  hashmap  14356  hashfun  14358  hashbclem  14373  hashf1lem2  14377  hashf1  14378  hash2prde  14391  prprrab  14394  hash3tpexb  14415  fi1uzind  14428  brfi1indALT  14431  s3sndisj  14888  s3iunsndisj  14889  rexfiuz  15269  fsumabs  15722  incexclem  15757  fprodcllemf  15879  fprodmodd  15918  iserodd  16761  hashbc0  16931  0ram  16946  ramub1  16954  initoid  17923  termoid  17924  equivestrcsetc  18073  gsumwspan  18769  gsmsymgrfix  19355  symgfixf1  19364  frgpnabllem1  19800  telgsums  19920  opprsubg  20286  subrngpropd  20499  subrgpropd  20539  coe1fzgsumdlem  22245  evl1gsumdlem  22298  mdetunilem9  22562  topnex  22938  neitr  23122  ordtbas2  23133  pnfnei  23162  mnfnei  23163  hauscmplem  23348  2ndcsb  23391  2ndcsep  23401  ptpjopn  23554  snfil  23806  fbasrn  23826  rnelfmlem  23894  rnelfm  23895  fmfnfmlem3  23898  fmfnfmlem4  23899  fmfnfm  23900  fclscmp  23972  alexsubALTlem4  23992  ptcmplem2  23995  symgtgp  24048  ustfilxp  24155  restutopopn  24180  ustuqtop2  24184  utopsnneiplem  24189  imasdsf1olem  24315  xpsdsval  24323  metuel2  24507  metustbl  24508  restmetu  24512  xrtgioo  24749  minveclem3b  25382  ovoliunlem1  25457  uniioombllem3  25540  itg1addlem4  25654  dvnff  25879  dvfsumlem3  25989  logfac  26564  gausslemma2dlem1a  27330  onsis  28239  umgrislfupgrlem  29144  lfuhgr1v0e  29276  cplgrop  29459  finsumvtxdg2size  29573  rgrusgrprc  29612  elwspths2spth  29992  fusgr2wsp2nb  30358  h2hlm  31004  axhcompl-zf  31022  opsbc2ie  32499  inpr0  32556  iuninc  32584  disjpreima  32608  suppss2f  32665  fnpreimac  32698  tocyccntz  33175  elrgspnlem1  33273  elrgspnlem2  33274  nsgqusf1olem2  33444  nsgqusf1olem3  33445  zarclsiin  33977  esumpfinvalf  34182  measiuns  34323  bnj23  34823  bnj110  34963  bnj1123  35091  bnj1373  35135  fineqvnttrclse  35229  lfuhgr2  35262  lfuhgr3  35263  acycgr1v  35292  umgracycusgr  35297  cusgracyclt3v  35299  dmopab3rexdif  35548  wzel  35965  dfrdg4  36094  bj-sbeq  37045  bj-sbel1  37049  bj-snsetex  37107  bj-snglc  37113  bj-taginv  37130  bj-adjfrombun  37190  poimirlem16  37776  poimirlem19  37779  eldmres  38409  ecres  38417  eldmqsres  38425  inxprnres  38430  cnvepres  38436  idinxpss  38450  inxpssidinxp  38454  idinxpssinxp  38455  cnvref5  38483  alrmomorn  38490  alrmomodm  38491  ssdmral  38503  brxrn  38507  dfxrn2  38509  dmcnvep  38512  inxpxrn  38542  rnxrn  38545  rnxrnres  38546  rnxrncnvepres  38547  rnxrnidres  38548  blockadjliftmap  38572  dfsucmap3  38576  dmsucmap  38581  dfsuccl4  38587  coss1cnvres  38619  coss2cnvepres  38620  1cossres  38631  dfcoels  38632  refressn  38645  br1cossinidres  38651  br1cossincnvepres  38652  br1cossxrnidres  38653  br1cossxrncnvepres  38654  refrelcosslem  38664  coss0  38681  cossid  38682  br1cossxrncnvssrres  38700  dfrefrels2  38705  dfcnvrefrels2  38720  dfcnvrefrels3  38721  dfsymrels2  38737  dftrrels2  38771  eldmqs1cossres  38857  dfeldisj5  38919  disjres  38942  antisymrelres  38961  disjdmqsss  39000  disjdmqscossss  39001  mpets  39040  dmqsblocks  39051  prter2  39080  cdleme31sdnN  40586  evl1gprodd  42310  sn-iotalem  42419  inintabss  43761  inintabd  43762  cnvcnvintabd  43783  cnvintabd  43786  comptiunov2i  43889  cotrcltrcl  43908  corcltrcl  43922  cotrclrcl  43925  rr-grothprimbi  44478  rr-groth  44482  dfuniv2  44485  onfrALTlem4VD  45068  iinssiin  45315  iinssf  45324  iindif2f  45346  rnmptpr  45363  wessf1ornlem  45371  disjinfi  45378  rnmptlb  45429  rnmptbddlem  45430  rnmptbd2lem  45434  ellimcabssub0  45805  preimageiingt  46906  preimaleiinlt  46907  eusnsn  47214  dfdfat2  47316  iineq0  49007  iinxp  49018  mofeu  49035  tposres0  49064  iinfsubc  49245  onsetreclem1  49892