Theorem ralrnmpt3

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

	Ref	Expression
Hypotheses	ralrnmpt3.1	$$⊢Ⅎx\phi$$
	ralrnmpt3.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	ralrnmpt3.3	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ralrnmpt3	$$⊢\phi \to \left(\forall y\in \mathrm{ran}\left(x\in A⟼B\right)\psi \leftrightarrow \forall x\in A\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralrnmpt3.1	$$⊢Ⅎx\phi$$
2		ralrnmpt3.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
3		ralrnmpt3.3	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
4	1 2	ralrimia	$$⊢\phi \to \forall x\in AB\in V$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	5 3	ralrnmptw	$$⊢\forall x\in AB\in V\to \left(\forall y\in \mathrm{ran}\left(x\in A⟼B\right)\psi \leftrightarrow \forall x\in A\chi \right)$$
7	4 6	syl	$$⊢\phi \to \left(\forall y\in \mathrm{ran}\left(x\in A⟼B\right)\psi \leftrightarrow \forall x\in A\chi \right)$$