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 | ||
|---|---|---|---|
| Assertion | fvelima | ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( 𝐹 “ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funbrfv | ⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝐴 ) ) | |
| 2 | 1 | reximdv | ⊢ ( Fun 𝐹 → ( ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐴 ) ) |
| 3 | elimag | ⊢ ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) → ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 ) ) | |
| 4 | 3 | ibi | ⊢ ( 𝐴 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 𝐴 ) |
| 5 | 2 4 | impel | ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( 𝐹 “ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐴 ) |