Theorem funfvima2 5940

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

Step	Hyp	Ref	Expression
1		ssel 3338	. . 3 |- ( A C_ dom F -> ( B e. A -> B e. dom F ) )
2		funfvima 5939	. . . . . 6 |- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )
3	2	ex 434	. . . . 5 |- ( Fun F -> ( B e. dom F -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
4	3	com23 78	. . . 4 |- ( Fun F -> ( B e. A -> ( B e. dom F -> ( F ` B ) e. ( F " A ) ) ) )
5	4	a2d 26	. . 3 |- ( Fun F -> ( ( B e. A -> B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
6	1, 5	syl5 32	. 2 |- ( Fun F -> ( A C_ dom F -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
7	6	imp 429	1 |- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1755   C_ wss 3316   dom cdm 4827   "cima 4830   Fun wfun 5400   ` cfv 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-fv 5414

This theorem is referenced by:  fnfvima  5942  f1oweALT  6550  tz7.49  6886  phimullem  13837  mrcuni  14542  frlmsslsp  18065  frlmsslspOLD  18066  lindfrn  18092  iscldtop  18541  1stcfb  18891  2ndcomap  18904  rnelfm  19368  fmfnfmlem2  19370  fmfnfmlem4  19372  qtopbaslem  20179  tgqioo  20219  bndth  20372  volsup  20879  dyadmbllem  20921  opnmbllem  20923  itg1addlem4  21019  c1liplem1  21310  dvcnvrelem1  21331  dvcnvrelem2  21332  plyco0  21545  plyaddlem1  21566  plymullem1  21567  dvloglem  21978  logf1o2  21980  efopn  21988  axcontlem10  23042  eupares  23419  imaelshi  25285  funimass4f  25775  sitgclg  26576  cvmliftlem3  27024  nocvxminlem  27678  nocvxmin  27679  opnmbllem0  28271  ivthALT  28374  ismtyres  28551  heibor1lem  28552  ismrc  28882  aomclem4  29255