Metamath Proof Explorer

Theorem fvelima2

Description: Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion fvelima2 
|- ( ( F Fn A /\ B e. ( F " C ) ) -> E. x e. ( A i^i C ) ( F ` x ) = B )

Proof

Step Hyp Ref Expression
1 elimag 
 |-  ( B e. ( F " C ) -> ( B e. ( F " C ) <-> E. x e. C x F B ) )
2 1 ibi 
 |-  ( B e. ( F " C ) -> E. x e. C x F B )
3 df-rex 
 |-  ( E. x e. C x F B <-> E. x ( x e. C /\ x F B ) )
4 2 3 sylib 
 |-  ( B e. ( F " C ) -> E. x ( x e. C /\ x F B ) )
5 fnbr 
 |-  ( ( F Fn A /\ x F B ) -> x e. A )
6 5 adantrl 
 |-  ( ( F Fn A /\ ( x e. C /\ x F B ) ) -> x e. A )
7 simprl 
 |-  ( ( F Fn A /\ ( x e. C /\ x F B ) ) -> x e. C )
8 6 7 elind 
 |-  ( ( F Fn A /\ ( x e. C /\ x F B ) ) -> x e. ( A i^i C ) )
9 fnfun 
 |-  ( F Fn A -> Fun F )
10 funbrfv 
 |-  ( Fun F -> ( x F B -> ( F ` x ) = B ) )
11 10 imp 
 |-  ( ( Fun F /\ x F B ) -> ( F ` x ) = B )
12 9 11 sylan 
 |-  ( ( F Fn A /\ x F B ) -> ( F ` x ) = B )
13 12 adantrl 
 |-  ( ( F Fn A /\ ( x e. C /\ x F B ) ) -> ( F ` x ) = B )
14 8 13 jca 
 |-  ( ( F Fn A /\ ( x e. C /\ x F B ) ) -> ( x e. ( A i^i C ) /\ ( F ` x ) = B ) )
15 14 ex 
 |-  ( F Fn A -> ( ( x e. C /\ x F B ) -> ( x e. ( A i^i C ) /\ ( F ` x ) = B ) ) )
16 15 eximdv 
 |-  ( F Fn A -> ( E. x ( x e. C /\ x F B ) -> E. x ( x e. ( A i^i C ) /\ ( F ` x ) = B ) ) )
17 16 imp 
 |-  ( ( F Fn A /\ E. x ( x e. C /\ x F B ) ) -> E. x ( x e. ( A i^i C ) /\ ( F ` x ) = B ) )
18 df-rex 
 |-  ( E. x e. ( A i^i C ) ( F ` x ) = B <-> E. x ( x e. ( A i^i C ) /\ ( F ` x ) = B ) )
19 17 18 sylibr 
 |-  ( ( F Fn A /\ E. x ( x e. C /\ x F B ) ) -> E. x e. ( A i^i C ) ( F ` x ) = B )
20 4 19 sylan2 
 |-  ( ( F Fn A /\ B e. ( F " C ) ) -> E. x e. ( A i^i C ) ( F ` x ) = B )