Theorem elv 3434

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  csbconstg  3856  csbvarg  4374  iinconst  4944  iuniin  4946  iinssiun  4947  iinss1  4949  ssiinf  4997  iinss  4999  iinss2  5000  iinab  5010  iinun2  5015  iundif2  5016  iindif1  5017  iindif2  5019  iinin2  5020  iinpw  5048  brab1  5133  triin  5209  eusvnf  5334  sbcop  5442  iunopab  5514  pwvabrel  5682  ssrel  5739  xpiindi  5790  dmopab2rex  5872  dfima2  6027  args  6057  inisegn0  6063  dffr3  6064  dfse2  6065  cnv0  6103  dfco2a  6210  dfpo2  6260  iotaval2  6469  iinpreima  7021  tfinds2  7815  fvresex  7913  sbcoteq1a  8004  fnse  8083  xpord2pred  8095  xpord3lem  8099  xpord3pred  8102  suppvalbr  8114  cnvimadfsn  8122  reldmtpos  8184  rntpos  8189  ovtpos  8191  dftpos3  8194  tpostpos  8196  fprlem2  8251  onovuni  8282  oarec  8497  eqerlem  8679  elecreseq  8693  ixpiin  8872  ixpsnf1o  8886  boxriin  8888  idssen  8944  unxpdomlem3  9168  ac6sfi  9194  unbnn2  9207  fifo  9345  inf0  9542  ttrclselem2  9647  ttrclse  9648  rankxpsuc  9806  tcrank  9808  harcard  9902  infxpenlem  9935  infpwfien  9984  alephcard  9992  dfac3  10043  cflm  10172  fin23lem34  10268  dffin7-2  10320  fin1a2lem13  10334  itunitc1  10342  itunitc  10343  ituniiun  10344  hsmexlem4  10351  fin41  10366  axdclem2  10442  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  canthwe  10574  pwfseqlem5  10586  axgroth2  10748  axgroth6  10751  grothac  10753  grothtsk  10758  seqfeq4  14013  serle  14019  seqof  14021  hash1snb  14381  hashmap  14397  hashfun  14399  hashbclem  14414  hashf1lem2  14418  hashf1  14419  hash2prde  14432  prprrab  14435  hash3tpexb  14456  fi1uzind  14469  brfi1indALT  14472  s3sndisj  14929  s3iunsndisj  14930  rexfiuz  15310  fsumabs  15764  incexclem  15801  fprodcllemf  15923  fprodmodd  15962  iserodd  16806  hashbc0  16976  0ram  16991  ramub1  16999  initoid  17968  termoid  17969  equivestrcsetc  18118  gsumwspan  18814  gsmsymgrfix  19403  symgfixf1  19412  frgpnabllem1  19848  telgsums  19968  opprsubg  20332  subrngpropd  20545  subrgpropd  20585  coe1fzgsumdlem  22268  evl1gsumdlem  22321  mdetunilem9  22585  topnex  22961  neitr  23145  ordtbas2  23156  pnfnei  23185  mnfnei  23186  hauscmplem  23371  2ndcsb  23414  2ndcsep  23424  ptpjopn  23577  snfil  23829  fbasrn  23849  rnelfmlem  23917  rnelfm  23918  fmfnfmlem3  23921  fmfnfmlem4  23922  fmfnfm  23923  fclscmp  23995  alexsubALTlem4  24015  ptcmplem2  24018  symgtgp  24071  ustfilxp  24178  restutopopn  24203  ustuqtop2  24207  utopsnneiplem  24212  imasdsf1olem  24338  xpsdsval  24346  metuel2  24530  metustbl  24531  restmetu  24535  xrtgioo  24772  minveclem3b  25395  ovoliunlem1  25469  uniioombllem3  25552  itg1addlem4  25666  dvnff  25890  dvfsumlem3  25995  logfac  26565  gausslemma2dlem1a  27328  onsis  28266  ons2ind  28267  umgrislfupgrlem  29191  lfuhgr1v0e  29323  cplgrop  29506  finsumvtxdg2size  29619  rgrusgrprc  29658  elwspths2spth  30038  fusgr2wsp2nb  30404  h2hlm  31051  axhcompl-zf  31069  opsbc2ie  32545  inpr0  32602  iuninc  32630  disjpreima  32654  suppss2f  32711  fnpreimac  32743  tocyccntz  33205  elrgspnlem1  33303  elrgspnlem2  33304  nsgqusf1olem2  33474  nsgqusf1olem3  33475  zarclsiin  34015  esumpfinvalf  34220  measiuns  34361  bnj23  34861  bnj110  35000  bnj1123  35128  bnj1373  35172  fineqvnttrclse  35268  lfuhgr2  35301  lfuhgr3  35302  acycgr1v  35331  umgracycusgr  35336  cusgracyclt3v  35338  dmopab3rexdif  35587  wzel  36004  dfrdg4  36133  bj-sbeq  37208  bj-sbel1  37212  bj-snsetex  37270  bj-snglc  37276  bj-taginv  37293  bj-adjfrombun  37353  poimirlem16  37957  poimirlem19  37960  eldmres  38598  ecres  38606  eldmqsres  38614  inxprnres  38619  cnvepres  38625  idinxpss  38639  inxpssidinxp  38643  idinxpssinxp  38644  cnvref5  38672  alrmomorn  38679  alrmomodm  38680  ssdmral  38700  brxrn  38704  dfxrn2  38706  dmcnvep  38709  inxpxrn  38739  rnxrn  38742  rnxrnres  38743  rnxrncnvepres  38744  rnxrnidres  38745  blockadjliftmap  38779  dfsucmap3  38784  dmsucmap  38789  dfsuccl4  38795  coss1cnvres  38828  coss2cnvepres  38829  1cossres  38840  dfcoels  38841  refressn  38854  br1cossinidres  38860  br1cossincnvepres  38861  br1cossxrnidres  38862  br1cossxrncnvepres  38863  refrelcosslem  38873  coss0  38890  cossid  38891  br1cossxrncnvssrres  38909  dfrefrels2  38914  dfcnvrefrels2  38929  dfcnvrefrels3  38930  dfsymrels2  38946  dftrrels2  38980  eldmqs1cossres  39065  disjimdmqseq  39130  dfeldisj5  39134  eldisjdmqsim  39138  disjres  39165  antisymrelres  39187  disjdmqsss  39226  disjdmqscossss  39227  mpets  39277  dmqsblocks  39288  dfpeters2  39295  prter2  39327  cdleme31sdnN  40833  evl1gprodd  42556  sn-iotalem  42662  inintabss  44005  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  comptiunov2i  44133  cotrcltrcl  44152  corcltrcl  44166  cotrclrcl  44169  rr-grothprimbi  44722  rr-groth  44726  dfuniv2  44729  onfrALTlem4VD  45312  iinssiin  45559  iinssf  45568  iindif2f  45590  rnmptpr  45607  wessf1ornlem  45615  disjinfi  45622  rnmptlb  45672  rnmptbddlem  45673  rnmptbd2lem  45677  ellimcabssub0  46047  preimageiingt  47148  preimaleiinlt  47149  eusnsn  47474  dfdfat2  47576  iineq0  49295  iinxp  49306  mofeu  49323  tposres0  49352  iinfsubc  49533  onsetreclem1  50180