![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvelima | Structured version Visualization version GIF version |
Description: Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42. (Contributed by NM, 29-Apr-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
fvelima | ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funbrfv 6691 | . . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴)) | |
2 | 1 | reximdv 3232 | . 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)) |
3 | elimag 5900 | . . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)) | |
4 | 3 | ibi 270 | . 2 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴) |
5 | 2, 4 | impel 509 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∃wrex 3107 class class class wbr 5030 “ cima 5522 Fun wfun 6318 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fv 6332 |
This theorem is referenced by: ssimaex 6723 isofrlem 7072 fimaproj 7812 tz7.49 8064 rankwflemb 9206 tcrank 9297 zorn2lem5 9911 zorn2lem6 9912 uniimadom 9955 wunr1om 10130 tskr1om 10178 tskr1om2 10179 grur1 10231 iscldtop 21700 kqfvima 22335 fmfnfmlem4 22562 fmfnfm 22563 qustgpopn 22725 cphsscph 23855 c1liplem1 24599 plypf1 24809 ltgseg 26390 axcontlem9 26766 uhgrspan1 27093 pthdlem2lem 27556 htthlem 28700 xrofsup 30518 tocyccntz 30836 rhmimaidl 31017 dimval 31089 dimvalfi 31090 txomap 31187 qtophaus 31189 erdszelem7 32557 erdszelem8 32558 mrsub0 32876 mrsubccat 32878 mrsubcn 32879 msubrn 32889 mthmblem 32940 ivthALT 33796 ftc2nc 35139 heibor1lem 35247 ismrc 39642 funimassd 41863 icccncfext 42529 dirkercncflem2 42746 smfpimbor1lem1 43430 |
Copyright terms: Public domain | W3C validator |