Theorem ralrnmpt3

Description: A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	ralrnmpt3.1	|- F/ x ph
	ralrnmpt3.2	|- ( ( ph /\ x e. A ) -> B e. V )
	ralrnmpt3.3	|- ( y = B -> ( ps <-> ch ) )
Assertion	ralrnmpt3	|- ( ph -> ( A. y e. ran ( x e. A |-> B ) ps <-> A. x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralrnmpt3.1	|- F/ x ph
2		ralrnmpt3.2	|- ( ( ph /\ x e. A ) -> B e. V )
3		ralrnmpt3.3	|- ( y = B -> ( ps <-> ch ) )
4	1 2	ralrimia	|- ( ph -> A. x e. A B e. V )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5 3	ralrnmptw	|- ( A. x e. A B e. V -> ( A. y e. ran ( x e. A |-> B ) ps <-> A. x e. A ch ) )
7	4 6	syl	|- ( ph -> ( A. y e. ran ( x e. A |-> B ) ps <-> A. x e. A ch ) )