This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fimarab

Description: Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Assertion fimarab 
|- ( ( F : A --> B /\ X C_ A ) -> ( F " X ) = { y e. B | E. x e. X ( F ` x ) = y } )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ( F : A --> B /\ X C_ A )
2 nfcv 
 |-  F/_ y ( F " X )
3 nfrab1 
 |-  F/_ y { y e. B | E. x e. X ( F ` x ) = y }
4 ffn 
 |-  ( F : A --> B -> F Fn A )
5 fvelimab 
 |-  ( ( F Fn A /\ X C_ A ) -> ( y e. ( F " X ) <-> E. x e. X ( F ` x ) = y ) )
6 5 anbi2d 
 |-  ( ( F Fn A /\ X C_ A ) -> ( ( y e. B /\ y e. ( F " X ) ) <-> ( y e. B /\ E. x e. X ( F ` x ) = y ) ) )
7 4 6 sylan 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( ( y e. B /\ y e. ( F " X ) ) <-> ( y e. B /\ E. x e. X ( F ` x ) = y ) ) )
8 fimass 
 |-  ( F : A --> B -> ( F " X ) C_ B )
9 8 adantr 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( F " X ) C_ B )
10 9 sseld 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( y e. ( F " X ) -> y e. B ) )
11 10 pm4.71rd 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( y e. ( F " X ) <-> ( y e. B /\ y e. ( F " X ) ) ) )
12 rabid 
 |-  ( y e. { y e. B | E. x e. X ( F ` x ) = y } <-> ( y e. B /\ E. x e. X ( F ` x ) = y ) )
13 12 a1i 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( y e. { y e. B | E. x e. X ( F ` x ) = y } <-> ( y e. B /\ E. x e. X ( F ` x ) = y ) ) )
14 7 11 13 3bitr4d 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( y e. ( F " X ) <-> y e. { y e. B | E. x e. X ( F ` x ) = y } ) )
15 1 2 3 14 eqrd 
 |-  ( ( F : A --> B /\ X C_ A ) -> ( F " X ) = { y e. B | E. x e. X ( F ` x ) = y } )