Theorem imassmpt

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	imassmpt.1	|- F/ x ph
	imassmpt.2	|- ( ( ph /\ x e. ( A i^i C ) ) -> B e. V )
	imassmpt.3	|- F = ( x e. A |-> B )
Assertion	imassmpt	|- ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )

Proof

Step	Hyp	Ref	Expression
1		imassmpt.1	|- F/ x ph
2		imassmpt.2	|- ( ( ph /\ x e. ( A i^i C ) ) -> B e. V )
3		imassmpt.3	|- F = ( x e. A |-> B )
4		df-ima	|- ( F " C ) = ran ( F |` C )
5	3	reseq1i	|- ( F |` C ) = ( ( x e. A |-> B ) |` C )
6		resmpt3	|- ( ( x e. A |-> B ) |` C ) = ( x e. ( A i^i C ) |-> B )
7	5 6	eqtri	|- ( F |` C ) = ( x e. ( A i^i C ) |-> B )
8	7	rneqi	|- ran ( F |` C ) = ran ( x e. ( A i^i C ) |-> B )
9	4 8	eqtri	|- ( F " C ) = ran ( x e. ( A i^i C ) |-> B )
10	9	sseq1i	|- ( ( F " C ) C_ D <-> ran ( x e. ( A i^i C ) |-> B ) C_ D )
11		eqid	|- ( x e. ( A i^i C ) |-> B ) = ( x e. ( A i^i C ) |-> B )
12	1 11 2	rnmptssbi	|- ( ph -> ( ran ( x e. ( A i^i C ) |-> B ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )
13	10 12	bitrid	|- ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )