Theorem elv 3484

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481

This theorem is referenced by:  csbconstg  3917  csbvarg  4433  iinconst  5001  iuniin  5003  iinssiun  5004  iinss1  5006  ssiinf  5053  iinss  5055  iinss2  5056  iinab  5067  iinun2  5072  iundif2  5073  iindif1  5074  iindif2  5076  iinin2  5077  iinpw  5105  brab1  5190  triin  5275  eusvnf  5391  sbcop  5493  iunopab  5563  pwvabrel  5735  ssrel  5791  difopabOLD  5840  xpiindi  5845  dmopab2rex  5927  dfima2  6079  args  6109  inisegn0  6115  dffr3  6116  dfse2  6117  dfco2a  6265  dfpo2  6315  iotaval2  6528  iotavalOLD  6534  iinpreima  7088  tfinds2  7886  fvresex  7985  sbcoteq1a  8077  fnse  8159  xpord2pred  8171  xpord3lem  8175  xpord3pred  8178  suppvalbr  8190  cnvimadfsn  8198  reldmtpos  8260  rntpos  8265  ovtpos  8267  dftpos3  8270  tpostpos  8272  fprlem2  8327  wfrlem10OLD  8359  onovuni  8383  oarec  8601  eqerlem  8781  ixpiin  8965  ixpsnf1o  8979  boxriin  8981  idssen  9038  unxpdomlem3  9289  ac6sfi  9321  unbnn2  9334  fifo  9473  inf0  9662  ttrclselem2  9767  ttrclse  9768  rankxpsuc  9923  tcrank  9925  harcard  10019  infxpenlem  10054  infpwfien  10103  alephcard  10111  dfac3  10162  cflm  10291  fin23lem34  10387  dffin7-2  10439  fin1a2lem13  10453  itunitc1  10461  itunitc  10462  ituniiun  10463  hsmexlem4  10470  fin41  10485  axdclem2  10561  fpwwe2lem11  10682  fpwwe2lem12  10683  fpwwe2  10684  canthwe  10692  pwfseqlem5  10704  axgroth2  10866  axgroth6  10869  grothac  10871  grothtsk  10876  seqfeq4  14093  serle  14099  seqof  14101  hash1snb  14459  hashmap  14475  hashfun  14477  hashbclem  14492  hashf1lem2  14496  hashf1  14497  hash2prde  14510  prprrab  14513  hash3tpexb  14534  fi1uzind  14547  brfi1indALT  14550  s3sndisj  15007  s3iunsndisj  15008  rexfiuz  15387  fsumabs  15838  incexclem  15873  fprodcllemf  15995  fprodmodd  16034  iserodd  16874  hashbc0  17044  0ram  17059  ramub1  17067  initoid  18047  termoid  18048  equivestrcsetc  18198  gsumwspan  18860  gsmsymgrfix  19447  symgfixf1  19456  frgpnabllem1  19892  telgsums  20012  opprsubg  20353  subrngpropd  20569  subrgpropd  20609  coe1fzgsumdlem  22308  evl1gsumdlem  22361  mdetunilem9  22627  topnex  23004  neitr  23189  ordtbas2  23200  pnfnei  23229  mnfnei  23230  hauscmplem  23415  2ndcsb  23458  2ndcsep  23468  ptpjopn  23621  snfil  23873  fbasrn  23893  rnelfmlem  23961  rnelfm  23962  fmfnfmlem3  23965  fmfnfmlem4  23966  fmfnfm  23967  fclscmp  24039  alexsubALTlem4  24059  ptcmplem2  24062  symgtgp  24115  ustfilxp  24222  restutopopn  24248  ustuqtop2  24252  utopsnneiplem  24257  imasdsf1olem  24384  xpsdsval  24392  metuel2  24579  metustbl  24580  restmetu  24584  xrtgioo  24829  minveclem3b  25463  ovoliunlem1  25538  uniioombllem3  25621  itg1addlem4  25735  dvnff  25960  dvfsumlem3  26070  logfac  26644  gausslemma2dlem1a  27410  umgrislfupgrlem  29140  lfuhgr1v0e  29272  cplgrop  29455  finsumvtxdg2size  29569  rgrusgrprc  29608  elwspths2spth  29988  fusgr2wsp2nb  30354  h2hlm  31000  axhcompl-zf  31018  opsbc2ie  32496  inpr0  32551  iuninc  32574  disjpreima  32598  suppss2f  32649  fnpreimac  32682  tocyccntz  33165  elrgspnlem1  33247  elrgspnlem2  33248  nsgqusf1olem2  33443  nsgqusf1olem3  33444  zarclsiin  33871  esumpfinvalf  34078  measiuns  34219  bnj23  34733  bnj110  34873  bnj1123  35001  bnj1373  35045  lfuhgr2  35125  lfuhgr3  35126  acycgr1v  35155  umgracycusgr  35160  cusgracyclt3v  35162  dmopab3rexdif  35411  wzel  35826  dfrdg4  35953  bj-sbeq  36903  bj-sbel1  36907  bj-snsetex  36965  bj-snglc  36971  bj-taginv  36988  bj-adjfrombun  37048  poimirlem16  37644  poimirlem19  37647  eldmres  38272  ecres  38280  ecres2  38281  eldmqsres  38289  inxprnres  38294  cnvepres  38300  idinxpss  38314  inxpssidinxp  38318  idinxpssinxp  38319  cnvref5  38353  alrmomorn  38360  alrmomodm  38361  brxrn  38376  dfxrn2  38378  inxpxrn  38397  rnxrn  38400  rnxrnres  38401  rnxrncnvepres  38402  rnxrnidres  38403  coss1cnvres  38419  coss2cnvepres  38420  1cossres  38431  dfcoels  38432  refressn  38445  br1cossinidres  38451  br1cossincnvepres  38452  br1cossxrnidres  38453  br1cossxrncnvepres  38454  refrelcosslem  38464  coss0  38481  cossid  38482  br1cossxrncnvssrres  38510  dfrefrels2  38515  dfcnvrefrels2  38530  dfcnvrefrels3  38531  dfsymrels2  38547  dftrrels2  38577  eldmqs1cossres  38661  dfeldisj5  38723  disjres  38746  antisymrelres  38765  disjdmqsss  38804  disjdmqscossss  38805  mpets  38844  prter2  38883  cdleme31sdnN  40390  evl1gprodd  42119  sn-iotalem  42261  inintabss  43596  inintabd  43597  cnvcnvintabd  43618  cnvintabd  43621  comptiunov2i  43724  cotrcltrcl  43743  corcltrcl  43757  cotrclrcl  43760  rr-grothprimbi  44319  rr-groth  44323  dfuniv2  44326  onfrALTlem4VD  44911  iinssiin  45139  iinssf  45148  iindif2f  45170  rnmptpr  45187  wessf1ornlem  45195  disjinfi  45202  rnmptlb  45255  rnmptbddlem  45256  rnmptbd2lem  45260  ellimcabssub0  45637  eusnsn  47043  dfdfat2  47145  mofeu  48762  tposres0  48783  onsetreclem1  49279