![]() |
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 7227 | . . . . 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 3970 | . 2 ⊢ (𝐴 ⊆ dom 𝐹 → (𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹)) | |
6 | 4, 5 | impel 505 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2098 ⊆ wss 3943 dom cdm 5669 “ cima 5672 Fun wfun 6531 ‘cfv 6537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-opab 5204 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6489 df-fun 6539 df-fn 6540 df-fv 6545 |
This theorem is referenced by: funfvima2d 7229 fnfvima 7230 resfvresima 7232 f1oweALT 7958 tz7.49 8446 phimullem 16721 mrcuni 17574 frlmsslsp 21691 lindfrn 21716 iscldtop 22954 1stcfb 23304 2ndcomap 23317 rnelfm 23812 fmfnfmlem2 23814 fmfnfmlem4 23816 qtopbaslem 24630 tgqioo 24671 bndth 24839 volsup 25440 dyadmbllem 25483 opnmbllem 25485 itg1addlem4 25583 itg1addlem4OLD 25584 c1liplem1 25884 dvcnvrelem1 25905 dvcnvrelem2 25906 plyco0 26081 plyaddlem1 26102 plymullem1 26103 dvloglem 26537 logf1o2 26539 efopn 26547 nocvxminlem 27665 nocvxmin 27666 axcontlem10 28739 imaelshi 31820 funimass4f 32370 sitgclg 33871 cvmliftlem3 34806 ivthALT 35728 opnmbllem0 37037 ismtyres 37189 heibor1lem 37190 ismrc 42017 aomclem4 42377 |
Copyright terms: Public domain | W3C validator |