Theorem elimampt

Description: Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022)

	Ref	Expression
Hypotheses	elimampt.f	|- F = ( x e. A |-> B )
	elimampt.c	|- ( ph -> C e. W )
	elimampt.d	|- ( ph -> D C_ A )
Assertion	elimampt	|- ( ph -> ( C e. ( F " D ) <-> E. x e. D C = B ) )

Proof

Step	Hyp	Ref	Expression
1		elimampt.f	|- F = ( x e. A |-> B )
2		elimampt.c	|- ( ph -> C e. W )
3		elimampt.d	|- ( ph -> D C_ A )
4		df-ima	|- ( F " D ) = ran ( F |` D )
5	4	eleq2i	|- ( C e. ( F " D ) <-> C e. ran ( F |` D ) )
6	1	reseq1i	|- ( F |` D ) = ( ( x e. A |-> B ) |` D )
7		resmpt	|- ( D C_ A -> ( ( x e. A |-> B ) |` D ) = ( x e. D |-> B ) )
8	6 7	syl5eq	|- ( D C_ A -> ( F |` D ) = ( x e. D |-> B ) )
9	8	rneqd	|- ( D C_ A -> ran ( F |` D ) = ran ( x e. D |-> B ) )
10	9	eleq2d	|- ( D C_ A -> ( C e. ran ( F |` D ) <-> C e. ran ( x e. D |-> B ) ) )
11	3 10	syl	|- ( ph -> ( C e. ran ( F |` D ) <-> C e. ran ( x e. D |-> B ) ) )
12		eqid	|- ( x e. D |-> B ) = ( x e. D |-> B )
13	12	elrnmpt	|- ( C e. W -> ( C e. ran ( x e. D |-> B ) <-> E. x e. D C = B ) )
14	2 13	syl	|- ( ph -> ( C e. ran ( x e. D |-> B ) <-> E. x e. D C = B ) )
15	11 14	bitrd	|- ( ph -> ( C e. ran ( F |` D ) <-> E. x e. D C = B ) )
16	5 15	syl5bb	|- ( ph -> ( C e. ( F " D ) <-> E. x e. D C = B ) )