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  17939  termoid  17940  equivestrcsetc  18089  gsumwspan  18749  gsmsymgrfix  19334  symgfixf1  19343  frgpnabllem1  19779  telgsums  19899  opprsubg  20237  subrngpropd  20453  subrgpropd  20493  coe1fzgsumdlem  22166  evl1gsumdlem  22219  mdetunilem9  22483  topnex  22859  neitr  23043  ordtbas2  23054  pnfnei  23083  mnfnei  23084  hauscmplem  23269  2ndcsb  23312  2ndcsep  23322  ptpjopn  23475  snfil  23727  fbasrn  23747  rnelfmlem  23815  rnelfm  23816  fmfnfmlem3  23819  fmfnfmlem4  23820  fmfnfm  23821  fclscmp  23893  alexsubALTlem4  23913  ptcmplem2  23916  symgtgp  23969  ustfilxp  24076  restutopopn  24102  ustuqtop2  24106  utopsnneiplem  24111  imasdsf1olem  24237  xpsdsval  24245  metuel2  24429  metustbl  24430  restmetu  24434  xrtgioo  24671  minveclem3b  25304  ovoliunlem1  25379  uniioombllem3  25462  itg1addlem4  25576  dvnff  25801  dvfsumlem3  25911  logfac  26486  gausslemma2dlem1a  27252  onsis  28148  umgrislfupgrlem  29025  lfuhgr1v0e  29157  cplgrop  29340  finsumvtxdg2size  29454  rgrusgrprc  29493  elwspths2spth  29870  fusgr2wsp2nb  30236  h2hlm  30882  axhcompl-zf  30900  opsbc2ie  32378  inpr0  32434  iuninc  32462  disjpreima  32486  suppss2f  32535  fnpreimac  32568  tocyccntz  33074  elrgspnlem1  33166  elrgspnlem2  33167  nsgqusf1olem2  33358  nsgqusf1olem3  33359  zarclsiin  33834  esumpfinvalf  34039  measiuns  34180  bnj23  34681  bnj110  34821  bnj1123  34949  bnj1373  34993  lfuhgr2  35079  lfuhgr3  35080  acycgr1v  35109  umgracycusgr  35114  cusgracyclt3v  35116  dmopab3rexdif  35365  wzel  35785  dfrdg4  35912  bj-sbeq  36862  bj-sbel1  36866  bj-snsetex  36924  bj-snglc  36930  bj-taginv  36947  bj-adjfrombun  37007  poimirlem16  37603  poimirlem19  37606  eldmres  38232  ecres  38240  eldmqsres  38248  inxprnres  38253  cnvepres  38259  idinxpss  38273  inxpssidinxp  38277  idinxpssinxp  38278  cnvref5  38306  alrmomorn  38313  alrmomodm  38314  brxrn  38329  dfxrn2  38331  dmcnvep  38334  inxpxrn  38354  rnxrn  38357  rnxrnres  38358  rnxrncnvepres  38359  rnxrnidres  38360  coss1cnvres  38381  coss2cnvepres  38382  1cossres  38393  dfcoels  38394  refressn  38407  br1cossinidres  38413  br1cossincnvepres  38414  br1cossxrnidres  38415  br1cossxrncnvepres  38416  refrelcosslem  38426  coss0  38443  cossid  38444  br1cossxrncnvssrres  38472  dfrefrels2  38477  dfcnvrefrels2  38492  dfcnvrefrels3  38493  dfsymrels2  38509  dftrrels2  38539  eldmqs1cossres  38624  dfeldisj5  38686  disjres  38709  antisymrelres  38728  disjdmqsss  38767  disjdmqscossss  38768  mpets  38807  dmqsblocks  38818  prter2  38847  cdleme31sdnN  40354  evl1gprodd  42078  sn-iotalem  42182  inintabss  43540  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  comptiunov2i  43668  cotrcltrcl  43687  corcltrcl  43701  cotrclrcl  43704  rr-grothprimbi  44257  rr-groth  44261  dfuniv2  44264  onfrALTlem4VD  44848  iinssiin  45096  iinssf  45105  iindif2f  45127  rnmptpr  45144  wessf1ornlem  45152  disjinfi  45159  rnmptlb  45210  rnmptbddlem  45211  rnmptbd2lem  45215  ellimcabssub0  45588  eusnsn  47000  dfdfat2  47102  iineq0  48781  iinxp  48792  mofeu  48809  tposres0  48838  iinfsubc  49020  onsetreclem1  49667