Theorem funfvima2 7229

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 7228	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))
2	1	ex 417	. . . 4 ⊢ (Fun 𝐹 → (𝐵 ∈ dom 𝐹 → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
3	2	com23 87	. . 3 ⊢ (Fun 𝐹 → (𝐵 ∈ 𝐴 → (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
4	3	a2d 30	. 2 ⊢ (Fun 𝐹 → ((𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))))
5		ssel 3931	. 2 ⊢ (𝐴 ⊆ dom 𝐹 → (𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹))
6	4, 5	impel 514	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3905  dom cdm 5661   “ cima 5664  Fun wfun 6530  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  funfvima2d  7230  fnfvima  7231  resfvresima  7233  f1oweALT  7965  tz7.49  8428  phimullem  16833  mrcuni  17672  frlmsslsp  21946  lindfrn  21971  iscldtop  23252  1stcfb  23602  2ndcomap  23615  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem4  24114  qtopbaslem  24915  tgqioo  24957  bndth  25117  volsup  25715  dyadmbllem  25758  opnmbllem  25760  itg1addlem4  25858  c1liplem1  26155  dvcnvrelem1  26176  dvcnvrelem2  26177  plyco0  26349  plyaddlem1  26370  plymullem1  26371  dvloglem  26813  logf1o2  26815  efopn  26823  nobdaymin  27946  nocvxminlem  27947  axcontlem10  29323  imaelshi  32410  funimass4f  32982  sitgclg  34732  cvmliftlem3  35779  ivthALT  36846  opnmbllem0  38307  ismtyres  38459  heibor1lem  38460  ismrc  43432  aomclem4  43784