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

Theorem funfvima2 5956
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 3353 . . 3  |-  ( A 
C_  dom  F  ->  ( B  e.  A  ->  B  e.  dom  F ) )
2 funfvima 5955 . . . . . 6  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( B  e.  A  ->  ( F `  B
)  e.  ( F
" A ) ) )
32ex 434 . . . . 5  |-  ( Fun 
F  ->  ( B  e.  dom  F  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A ) ) ) )
43com23 78 . . . 4  |-  ( Fun 
F  ->  ( B  e.  A  ->  ( B  e.  dom  F  -> 
( F `  B
)  e.  ( F
" A ) ) ) )
54a2d 26 . . 3  |-  ( Fun 
F  ->  ( ( B  e.  A  ->  B  e.  dom  F )  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A ) ) ) )
61, 5syl5 32 . 2  |-  ( Fun 
F  ->  ( A  C_ 
dom  F  ->  ( B  e.  A  ->  ( F `  B )  e.  ( F " A
) ) ) )
76imp 429 1  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( B  e.  A  ->  ( F `  B
)  e.  ( F
" A ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    C_ wss 3331   dom cdm 4843   "cima 4846   Fun wfun 5415   ` cfv 5421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-fv 5429
This theorem is referenced by:  fnfvima  5958  f1oweALT  6564  tz7.49  6903  phimullem  13857  mrcuni  14562  frlmsslsp  18226  frlmsslspOLD  18227  lindfrn  18253  iscldtop  18702  1stcfb  19052  2ndcomap  19065  rnelfm  19529  fmfnfmlem2  19531  fmfnfmlem4  19533  qtopbaslem  20340  tgqioo  20380  bndth  20533  volsup  21040  dyadmbllem  21082  opnmbllem  21084  itg1addlem4  21180  c1liplem1  21471  dvcnvrelem1  21492  dvcnvrelem2  21493  plyco0  21663  plyaddlem1  21684  plymullem1  21685  dvloglem  22096  logf1o2  22098  efopn  22106  axcontlem10  23222  eupares  23599  imaelshi  25465  funimass4f  25954  sitgclg  26731  cvmliftlem3  27179  nocvxminlem  27834  nocvxmin  27835  opnmbllem0  28430  ivthALT  28533  ismtyres  28710  heibor1lem  28711  ismrc  29040  aomclem4  29413
  Copyright terms: Public domain W3C validator