![]() |
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 6940 | . . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴)) | |
2 | 1 | reximdv 3171 | . 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)) |
3 | elimag 6062 | . . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)) | |
4 | 3 | ibi 267 | . 2 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴) |
5 | 2, 4 | impel 507 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 class class class wbr 5148 “ cima 5679 Fun wfun 6535 ‘cfv 6541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6493 df-fun 6543 df-fv 6549 |
This theorem is referenced by: funimassd 6956 ssimaex 6974 isofrlem 7334 fimaproj 8118 tz7.49 8442 rankwflemb 9785 tcrank 9876 zorn2lem5 10492 zorn2lem6 10493 uniimadom 10536 wunr1om 10711 tskr1om 10759 tskr1om2 10760 grur1 10812 imadrhmcl 20406 iscldtop 22591 kqfvima 23226 fmfnfmlem4 23453 fmfnfm 23454 qustgpopn 23616 cphsscph 24760 c1liplem1 25505 plypf1 25718 lrrecfr 27417 ltgseg 27837 axcontlem9 28220 uhgrspan1 28550 pthdlem2lem 29014 htthlem 30158 xrofsup 31968 tocyccntz 32291 rhmimaidl 32539 dimval 32675 dimvalfi 32676 txomap 32803 qtophaus 32805 erdszelem7 34177 erdszelem8 34178 mrsub0 34496 mrsubccat 34498 mrsubcn 34499 msubrn 34509 mthmblem 34560 ivthALT 35209 ftc2nc 36559 heibor1lem 36666 imacrhmcl 41087 ismrc 41425 icccncfext 44590 dirkercncflem2 44807 smfpimbor1lem1 45501 |
Copyright terms: Public domain | W3C validator |