Theorem funfvima2 7233

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3906  dom cdm 5663   “ cima 5666  Fun wfun 6534  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  funfvima2d  7234  fnfvima  7235  resfvresima  7237  f1oweALT  7971  tz7.49  8434  phimullem  16856  mrcuni  17695  frlmsslsp  21976  lindfrn  22001  iscldtop  23282  1stcfb  23632  2ndcomap  23646  rnelfm  24141  fmfnfmlem2  24143  fmfnfmlem4  24145  qtopbaslem  24946  tgqioo  24988  bndth  25148  volsup  25746  dyadmbllem  25789  opnmbllem  25791  itg1addlem4  25889  c1liplem1  26186  dvcnvrelem1  26207  dvcnvrelem2  26208  plyco0  26380  plyaddlem1  26401  plymullem1  26402  dvloglem  26844  logf1o2  26846  efopn  26854  nobdaymin  27977  nocvxminlem  27978  axcontlem10  29354  imaelshi  32457  funimass4f  33029  sitgclg  34773  cvmliftlem3  35792  ivthALT  36879  opnmbllem0  38340  ismtyres  38492  heibor1lem  38493  ismrc  43465  aomclem4  43817