MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funfvima2 Unicode version

Theorem funfvima2 5795
Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.)
Assertion
Ref Expression
funfvima2  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( B  e.  A  ->  ( F `  B
)  e.  ( F
" A ) ) )

Proof of Theorem funfvima2
StepHypRef Expression
1 ssel 3208 . . 3  |-  ( A 
C_  dom  F  ->  ( B  e.  A  ->  B  e.  dom  F ) )
2 funfvima 5794 . . . . . 6  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( B  e.  A  ->  ( F `  B
)  e.  ( F
" A ) ) )
32ex 423 . . . . 5  |-  ( Fun 
F  ->  ( B  e.  dom  F  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A ) ) ) )
43com23 72 . . . 4  |-  ( Fun 
F  ->  ( B  e.  A  ->  ( B  e.  dom  F  -> 
( F `  B
)  e.  ( F
" A ) ) ) )
54a2d 23 . . 3  |-  ( Fun 
F  ->  ( ( B  e.  A  ->  B  e.  dom  F )  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A ) ) ) )
61, 5syl5 28 . 2  |-  ( Fun 
F  ->  ( A  C_ 
dom  F  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A
) ) ) )
76imp 418 1  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( B  e.  A  ->  ( F `  B
)  e.  ( F
" A ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701    C_ wss 3186   dom cdm 4726   "cima 4729   Fun wfun 5286   ` cfv 5292
This theorem is referenced by:  fnfvima  5797  f1oweALT  5893  tz7.49  6499  phimullem  12894  mrcuni  13572  iscldtop  16888  1stcfb  17227  2ndcomap  17240  rnelfm  17700  fmfnfmlem2  17702  fmfnfmlem4  17704  qtopbaslem  18319  tgqioo  18358  bndth  18509  volsup  18966  dyadmbllem  19007  opnmbllem  19009  itg1addlem4  19107  c1liplem1  19396  dvcnvrelem1  19417  dvcnvrelem2  19418  plyco0  19627  plyaddlem1  19648  plymullem1  19649  dvloglem  20048  logf1o2  20050  efopn  20058  imaelshi  22693  funimass4f  23194  cvmliftlem3  24102  eupares  24183  nocvxminlem  24729  nocvxmin  24730  axcontlem10  24987  ivthALT  25407  ismtyres  25680  heibor1lem  25681  ismrc  25924  aomclem4  26302  frlmsslsp  26396  lindfrn  26439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-fv 5300
  Copyright terms: Public domain W3C validator