Theorem rnmptssbi

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	rnmptssbi.1	|- F/ x ph
	rnmptssbi.2	|- F = ( x e. A |-> B )
	rnmptssbi.3	|- ( ( ph /\ x e. A ) -> B e. V )
Assertion	rnmptssbi	|- ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptssbi.1	|- F/ x ph
2		rnmptssbi.2	|- F = ( x e. A |-> B )
3		rnmptssbi.3	|- ( ( ph /\ x e. A ) -> B e. V )
4		nfmpt1	|- F/_ x ( x e. A |-> B )
5	2 4	nfcxfr	|- F/_ x F
6	5	nfrn	|- F/_ x ran F
7		nfcv	|- F/_ x C
8	6 7	nfss	|- F/ x ran F C_ C
9	1 8	nfan	|- F/ x ( ph /\ ran F C_ C )
10		simplr	|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> ran F C_ C )
11		simpr	|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> x e. A )
12	3	adantlr	|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. V )
13	2 11 12	elrnmpt1d	|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. ran F )
14	10 13	sseldd	|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. C )
15	9 14	ralrimia	|- ( ( ph /\ ran F C_ C ) -> A. x e. A B e. C )
16	2	rnmptss	|- ( A. x e. A B e. C -> ran F C_ C )
17	16	adantl	|- ( ( ph /\ A. x e. A B e. C ) -> ran F C_ C )
18	15 17	impbida	|- ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) )