Metamath Proof Explorer

Theorem fvelimab

Description: Function value in an image. (Contributed by NM, 20-Jan-2007) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by David Abernethy, 17-Dec-2011)

Ref Expression
Assertion fvelimab ⊢ F Fn A ∧ B ⊆ A → C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C

Proof

Step Hyp Ref Expression
1 elex ⊢ C ∈ F B → C ∈ V
2 1 anim2i ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ F B → F Fn A ∧ B ⊆ A ∧ C ∈ V
3 fvex ⊢ F ⁡ x ∈ V
4 eleq1 ⊢ F ⁡ x = C → F ⁡ x ∈ V ↔ C ∈ V
5 3 4 mpbii ⊢ F ⁡ x = C → C ∈ V
6 5 rexlimivw ⊢ ∃ x ∈ B F ⁡ x = C → C ∈ V
7 6 anim2i ⊢ F Fn A ∧ B ⊆ A ∧ ∃ x ∈ B F ⁡ x = C → F Fn A ∧ B ⊆ A ∧ C ∈ V
8 eleq1 ⊢ y = C → y ∈ F B ↔ C ∈ F B
9 eqeq2 ⊢ y = C → F ⁡ x = y ↔ F ⁡ x = C
10 9 rexbidv ⊢ y = C → ∃ x ∈ B F ⁡ x = y ↔ ∃ x ∈ B F ⁡ x = C
11 8 10 bibi12d ⊢ y = C → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y ↔ C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C
12 11 imbi2d ⊢ y = C → F Fn A ∧ B ⊆ A → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y ↔ F Fn A ∧ B ⊆ A → C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C
13 fnfun ⊢ F Fn A → Fun ⁡ F
14 fndm ⊢ F Fn A → dom ⁡ F = A
15 14 sseq2d ⊢ F Fn A → B ⊆ dom ⁡ F ↔ B ⊆ A
16 15 biimpar ⊢ F Fn A ∧ B ⊆ A → B ⊆ dom ⁡ F
17 dfimafn ⊢ Fun ⁡ F ∧ B ⊆ dom ⁡ F → F B = y | ∃ x ∈ B F ⁡ x = y
18 13 16 17 syl2an2r ⊢ F Fn A ∧ B ⊆ A → F B = y | ∃ x ∈ B F ⁡ x = y
19 18 abeq2d ⊢ F Fn A ∧ B ⊆ A → y ∈ F B ↔ ∃ x ∈ B F ⁡ x = y
20 12 19 vtoclg ⊢ C ∈ V → F Fn A ∧ B ⊆ A → C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C
21 20 impcom ⊢ F Fn A ∧ B ⊆ A ∧ C ∈ V → C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C
22 2 7 21 pm5.21nd ⊢ F Fn A ∧ B ⊆ A → C ∈ F B ↔ ∃ x ∈ B F ⁡ x = C