Theorem funfvima2 7251

Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.)

Assertion

Ref	Expression
funfvima2	⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))

Proof of Theorem funfvima2

Step	Hyp	Ref	Expression
1		funfvima 7250	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))
2	1	ex 412	. . . 4 ⊢ (Fun 𝐹 → (𝐵 ∈ dom 𝐹 → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
3	2	com23 86	. . 3 ⊢ (Fun 𝐹 → (𝐵 ∈ 𝐴 → (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
4	3	a2d 29	. 2 ⊢ (Fun 𝐹 → ((𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
5		ssel 3989	. 2 ⊢ (𝐴 ⊆ dom 𝐹 → (𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹))
6	4, 5	impel 505	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106   ⊆ wss 3963  dom cdm 5689   “ cima 5692  Fun wfun 6557  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  funfvima2d  7252  fnfvima  7253  resfvresima  7255  f1oweALT  7996  tz7.49  8484  phimullem  16813  mrcuni  17666  frlmsslsp  21834  lindfrn  21859  iscldtop  23119  1stcfb  23469  2ndcomap  23482  rnelfm  23977  fmfnfmlem2  23979  fmfnfmlem4  23981  qtopbaslem  24795  tgqioo  24836  bndth  25004  volsup  25605  dyadmbllem  25648  opnmbllem  25650  itg1addlem4  25748  itg1addlem4OLD  25749  c1liplem1  26050  dvcnvrelem1  26071  dvcnvrelem2  26072  plyco0  26246  plyaddlem1  26267  plymullem1  26268  dvloglem  26705  logf1o2  26707  efopn  26715  nocvxminlem  27837  nocvxmin  27838  axcontlem10  29003  imaelshi  32087  funimass4f  32654  sitgclg  34324  cvmliftlem3  35272  ivthALT  36318  opnmbllem0  37643  ismtyres  37795  heibor1lem  37796  ismrc  42689  aomclem4  43046