![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funfvima2 | Structured version Visualization version GIF version |
Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
Ref | Expression |
---|---|
funfvima2 | ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funfvima 6764 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | |
2 | 1 | ex 403 | . . . 4 ⊢ (Fun 𝐹 → (𝐵 ∈ dom 𝐹 → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))) |
3 | 2 | com23 86 | . . 3 ⊢ (Fun 𝐹 → (𝐵 ∈ 𝐴 → (𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))) |
4 | 3 | a2d 29 | . 2 ⊢ (Fun 𝐹 → ((𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴)))) |
5 | ssel 3815 | . 2 ⊢ (𝐴 ⊆ dom 𝐹 → (𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹)) | |
6 | 4, 5 | impel 501 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 ⊆ wss 3792 dom cdm 5355 “ cima 5358 Fun wfun 6129 ‘cfv 6135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-iota 6099 df-fun 6137 df-fn 6138 df-fv 6143 |
This theorem is referenced by: fnfvimad 6766 resfvresima 6767 fnfvima 6769 f1oweALT 7429 tz7.49 7823 phimullem 15888 mrcuni 16667 frlmsslsp 20539 lindfrn 20564 iscldtop 21307 1stcfb 21657 2ndcomap 21670 rnelfm 22165 fmfnfmlem2 22167 fmfnfmlem4 22169 qtopbaslem 22970 tgqioo 23011 bndth 23165 volsup 23760 dyadmbllem 23803 opnmbllem 23805 itg1addlem4 23903 c1liplem1 24196 dvcnvrelem1 24217 dvcnvrelem2 24218 plyco0 24385 plyaddlem1 24406 plymullem1 24407 dvloglem 24831 logf1o2 24833 efopn 24841 axcontlem10 26322 imaelshi 29489 funimass4f 30002 sitgclg 31002 cvmliftlem3 31868 nocvxminlem 32482 nocvxmin 32483 ivthALT 32918 opnmbllem0 34071 ismtyres 34231 heibor1lem 34232 ismrc 38224 aomclem4 38586 funfvima2d 39425 |
Copyright terms: Public domain | W3C validator |