Theorem elv 3441

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  csbconstg  3864  csbvarg  4381  iinconst  4950  iuniin  4952  iinssiun  4953  iinss1  4955  ssiinf  5001  iinss  5003  iinss2  5004  iinab  5014  iinun2  5019  iundif2  5020  iindif1  5021  iindif2  5023  iinin2  5024  iinpw  5052  brab1  5137  triin  5212  eusvnf  5328  sbcop  5427  iunopab  5497  pwvabrel  5665  ssrel  5722  xpiindi  5774  dmopab2rex  5856  dfima2  6010  args  6040  inisegn0  6046  dffr3  6047  dfse2  6048  cnv0  6086  dfco2a  6193  dfpo2  6243  iotaval2  6452  iinpreima  7002  tfinds2  7794  fvresex  7892  sbcoteq1a  7983  fnse  8063  xpord2pred  8075  xpord3lem  8079  xpord3pred  8082  suppvalbr  8094  cnvimadfsn  8102  reldmtpos  8164  rntpos  8169  ovtpos  8171  dftpos3  8174  tpostpos  8176  fprlem2  8231  onovuni  8262  oarec  8477  eqerlem  8657  elecreseq  8671  ixpiin  8848  ixpsnf1o  8862  boxriin  8864  idssen  8919  unxpdomlem3  9142  ac6sfi  9168  unbnn2  9181  fifo  9316  inf0  9511  ttrclselem2  9616  ttrclse  9617  rankxpsuc  9775  tcrank  9777  harcard  9871  infxpenlem  9904  infpwfien  9953  alephcard  9961  dfac3  10012  cflm  10141  fin23lem34  10237  dffin7-2  10289  fin1a2lem13  10303  itunitc1  10311  itunitc  10312  ituniiun  10313  hsmexlem4  10320  fin41  10335  axdclem2  10411  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  canthwe  10542  pwfseqlem5  10554  axgroth2  10716  axgroth6  10719  grothac  10721  grothtsk  10726  seqfeq4  13958  serle  13964  seqof  13966  hash1snb  14326  hashmap  14342  hashfun  14344  hashbclem  14359  hashf1lem2  14363  hashf1  14364  hash2prde  14377  prprrab  14380  hash3tpexb  14401  fi1uzind  14414  brfi1indALT  14417  s3sndisj  14874  s3iunsndisj  14875  rexfiuz  15255  fsumabs  15708  incexclem  15743  fprodcllemf  15865  fprodmodd  15904  iserodd  16747  hashbc0  16917  0ram  16932  ramub1  16940  initoid  17908  termoid  17909  equivestrcsetc  18058  gsumwspan  18754  gsmsymgrfix  19340  symgfixf1  19349  frgpnabllem1  19785  telgsums  19905  opprsubg  20270  subrngpropd  20483  subrgpropd  20523  coe1fzgsumdlem  22218  evl1gsumdlem  22271  mdetunilem9  22535  topnex  22911  neitr  23095  ordtbas2  23106  pnfnei  23135  mnfnei  23136  hauscmplem  23321  2ndcsb  23364  2ndcsep  23374  ptpjopn  23527  snfil  23779  fbasrn  23799  rnelfmlem  23867  rnelfm  23868  fmfnfmlem3  23871  fmfnfmlem4  23872  fmfnfm  23873  fclscmp  23945  alexsubALTlem4  23965  ptcmplem2  23968  symgtgp  24021  ustfilxp  24128  restutopopn  24153  ustuqtop2  24157  utopsnneiplem  24162  imasdsf1olem  24288  xpsdsval  24296  metuel2  24480  metustbl  24481  restmetu  24485  xrtgioo  24722  minveclem3b  25355  ovoliunlem1  25430  uniioombllem3  25513  itg1addlem4  25627  dvnff  25852  dvfsumlem3  25962  logfac  26537  gausslemma2dlem1a  27303  onsis  28208  umgrislfupgrlem  29100  lfuhgr1v0e  29232  cplgrop  29415  finsumvtxdg2size  29529  rgrusgrprc  29568  elwspths2spth  29948  fusgr2wsp2nb  30314  h2hlm  30960  axhcompl-zf  30978  opsbc2ie  32455  inpr0  32512  iuninc  32540  disjpreima  32564  suppss2f  32620  fnpreimac  32653  tocyccntz  33113  elrgspnlem1  33209  elrgspnlem2  33210  nsgqusf1olem2  33379  nsgqusf1olem3  33380  zarclsiin  33884  esumpfinvalf  34089  measiuns  34230  bnj23  34730  bnj110  34870  bnj1123  34998  bnj1373  35042  fineqvnttrclse  35144  lfuhgr2  35163  lfuhgr3  35164  acycgr1v  35193  umgracycusgr  35198  cusgracyclt3v  35200  dmopab3rexdif  35449  wzel  35866  dfrdg4  35995  bj-sbeq  36945  bj-sbel1  36949  bj-snsetex  37007  bj-snglc  37013  bj-taginv  37030  bj-adjfrombun  37090  poimirlem16  37686  poimirlem19  37689  eldmres  38319  ecres  38327  eldmqsres  38335  inxprnres  38340  cnvepres  38346  idinxpss  38360  inxpssidinxp  38364  idinxpssinxp  38365  cnvref5  38393  alrmomorn  38400  alrmomodm  38401  ssdmral  38413  brxrn  38417  dfxrn2  38419  dmcnvep  38422  inxpxrn  38452  rnxrn  38455  rnxrnres  38456  rnxrncnvepres  38457  rnxrnidres  38458  blockadjliftmap  38482  dfsucmap3  38486  dmsucmap  38491  dfsuccl4  38497  coss1cnvres  38529  coss2cnvepres  38530  1cossres  38541  dfcoels  38542  refressn  38555  br1cossinidres  38561  br1cossincnvepres  38562  br1cossxrnidres  38563  br1cossxrncnvepres  38564  refrelcosslem  38574  coss0  38591  cossid  38592  br1cossxrncnvssrres  38610  dfrefrels2  38615  dfcnvrefrels2  38630  dfcnvrefrels3  38631  dfsymrels2  38647  dftrrels2  38681  eldmqs1cossres  38767  dfeldisj5  38829  disjres  38852  antisymrelres  38871  disjdmqsss  38910  disjdmqscossss  38911  mpets  38950  dmqsblocks  38961  prter2  38990  cdleme31sdnN  40496  evl1gprodd  42220  sn-iotalem  42324  inintabss  43681  inintabd  43682  cnvcnvintabd  43703  cnvintabd  43706  comptiunov2i  43809  cotrcltrcl  43828  corcltrcl  43842  cotrclrcl  43845  rr-grothprimbi  44398  rr-groth  44402  dfuniv2  44405  onfrALTlem4VD  44988  iinssiin  45236  iinssf  45245  iindif2f  45267  rnmptpr  45284  wessf1ornlem  45292  disjinfi  45299  rnmptlb  45350  rnmptbddlem  45351  rnmptbd2lem  45355  ellimcabssub0  45727  eusnsn  47136  dfdfat2  47238  iineq0  48930  iinxp  48941  mofeu  48958  tposres0  48987  iinfsubc  49169  onsetreclem1  49816