Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnvinran Structured version   Visualization version   GIF version

Theorem fnvinran 38073
Description: the function value belongs to its codomain. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypothesis
Ref Expression
fnvinran.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
fnvinran ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)

Proof of Theorem fnvinran
StepHypRef Expression
1 fnvinran.1 . 2 (𝜑𝐹:𝐴𝐵)
21ffvelrnda 6150 1 ((𝜑𝐶𝐴) → (𝐹𝐶) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1938  wf 5685  cfv 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-fv 5697
This theorem is referenced by:  rfcnpre1  38078  rfcnpre2  38090  rfcnpre3  38092  rfcnpre4  38093  fmulcl  38530  fmuldfeqlem1  38531  fmul01lt1  38535  mulc1cncfg  38538  expcnfg  38541  ditgeqiooicc  38741  itgiccshift  38761  stoweidlem12  38794  stoweidlem15  38797  stoweidlem16  38798  stoweidlem17  38799  stoweidlem19  38801  stoweidlem21  38803  stoweidlem23  38805  stoweidlem25  38807  stoweidlem29  38811  stoweidlem31  38813  stoweidlem32  38814  stoweidlem34  38816  stoweidlem36  38818  stoweidlem37  38819  stoweidlem40  38822  stoweidlem41  38823  stoweidlem42  38824  stoweidlem45  38827  stoweidlem47  38829  stoweidlem48  38830  stoweidlem51  38833  stoweidlem60  38842  stoweidlem61  38843  stoweidlem62  38844  fourierdlem14  38903  fourierdlem28  38917  fourierdlem37  38927  fourierdlem55  38945  fourierdlem67  38957  fourierdlem69  38959  fourierdlem77  38967  fourierdlem88  38978  fourierdlem93  38983  fourierdlem111  39001  etransclem32  39051  etransclem33  39052  etransclem34  39053
  Copyright terms: Public domain W3C validator