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 ⊢FFnA∧B⊆A→C∈FB↔∃x∈BF⁡x=C

Proof

Step Hyp Ref Expression
1 elex ⊢C∈FB→C∈V
2 1 anim2i ⊢FFnA∧B⊆A∧C∈FB→FFnA∧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∈BF⁡x=C→C∈V
7 6 anim2i ⊢FFnA∧B⊆A∧∃x∈BF⁡x=C→FFnA∧B⊆A∧C∈V
8 eleq1 ⊢y=C→y∈FB↔C∈FB
9 eqeq2 ⊢y=C→F⁡x=y↔F⁡x=C
10 9 rexbidv ⊢y=C→∃x∈BF⁡x=y↔∃x∈BF⁡x=C
11 8 10 bibi12d ⊢y=C→y∈FB↔∃x∈BF⁡x=y↔C∈FB↔∃x∈BF⁡x=C
12 11 imbi2d ⊢y=C→FFnA∧B⊆A→y∈FB↔∃x∈BF⁡x=y↔FFnA∧B⊆A→C∈FB↔∃x∈BF⁡x=C
13 fnfun ⊢FFnA→Fun⁡F
14 fndm ⊢FFnA→dom⁡F=A
15 14 sseq2d ⊢FFnA→B⊆dom⁡F↔B⊆A
16 15 biimpar ⊢FFnA∧B⊆A→B⊆dom⁡F
17 dfimafn ⊢Fun⁡F∧B⊆dom⁡F→FB=y|∃x∈BF⁡x=y
18 13 16 17 syl2an2r ⊢FFnA∧B⊆A→FB=y|∃x∈BF⁡x=y
19 18 eqabrd ⊢FFnA∧B⊆A→y∈FB↔∃x∈BF⁡x=y
20 12 19 vtoclg ⊢C∈V→FFnA∧B⊆A→C∈FB↔∃x∈BF⁡x=C
21 20 impcom ⊢FFnA∧B⊆A∧C∈V→C∈FB↔∃x∈BF⁡x=C
22 2 7 21 pm5.21nd ⊢FFnA∧B⊆A→C∈FB↔∃x∈BF⁡x=C