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 } )