Theorem fnvinran 37331

Description: the function value belongs to its codomain. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Hypothesis

Ref	Expression
fnvinran.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
fnvinran	|- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Proof of Theorem fnvinran

Step	Hyp	Ref	Expression
1		fnvinran.1	. 2 |- ( ph -> F : A --> B )
2	1	ffvelrnda 6005	1 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1890   -->wf 5556   ` cfv 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pr 4611

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-id 4726  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-fv 5568

This theorem is referenced by:  rfcnpre1  37336  rfcnpre2  37348  rfcnpre3  37350  rfcnpre4  37351  fmulcl  37700  fmuldfeqlem1  37701  fmul01lt1  37705  mulc1cncfg  37708  expcnfg  37712  ditgeqiooicc  37878  itgiccshift  37898  stoweidlem12  37928  stoweidlem15  37931  stoweidlem16  37932  stoweidlem17  37933  stoweidlem19  37935  stoweidlem21  37937  stoweidlem23  37939  stoweidlem25  37941  stoweidlem29  37945  stoweidlem29OLD  37946  stoweidlem31  37948  stoweidlem32  37949  stoweidlem34  37951  stoweidlem36  37953  stoweidlem37  37954  stoweidlem40  37957  stoweidlem41  37958  stoweidlem42  37959  stoweidlem45  37962  stoweidlem47  37964  stoweidlem48  37965  stoweidlem51  37968  stoweidlem60  37977  stoweidlem61  37978  stoweidlem62  37979  stoweidlem62OLD  37980  fourierdlem14  38039  fourierdlem28  38053  fourierdlem37  38063  fourierdlem55  38081  fourierdlem67  38093  fourierdlem69  38095  fourierdlem77  38103  fourierdlem88  38114  fourierdlem93  38119  fourierdlem111  38137  etransclem32  38187  etransclem33  38188  etransclem34  38189