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

Theorem fnvinran 29860
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
StepHypRef Expression
1 fnvinran.1 . 2  |-  ( ph  ->  F : A --> B )
21ffvelrnda 5928 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1757   -->wf 5498   ` cfv 5502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-id 4720  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-fv 5510
This theorem is referenced by:  rfcnpre1  29865  rfcnpre2  29877  rfcnpre3  29879  rfcnpre4  29880  fmulcl  29886  fmuldfeqlem1  29887  fmul01lt1  29891  mulc1cncfg  29894  expcnfg  29897  stoweidlem12  29931  stoweidlem15  29934  stoweidlem16  29935  stoweidlem17  29936  stoweidlem19  29938  stoweidlem21  29940  stoweidlem23  29942  stoweidlem25  29944  stoweidlem29  29948  stoweidlem31  29950  stoweidlem32  29951  stoweidlem34  29953  stoweidlem36  29955  stoweidlem37  29956  stoweidlem40  29959  stoweidlem41  29960  stoweidlem42  29961  stoweidlem45  29964  stoweidlem47  29966  stoweidlem48  29967  stoweidlem51  29970  stoweidlem60  29979  stoweidlem61  29980  stoweidlem62  29981
  Copyright terms: Public domain W3C validator