Theorem ralrnmptw

Description: A restricted quantifier over an image set. Version of ralrnmpt with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	ralrnmptw.1	$$⊢F=\left(x\in A⟼B\right)$$
	ralrnmptw.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ralrnmptw	$$⊢\forall x\in AB\in V\to \left(\forall y\in \mathrm{ran}F\psi \leftrightarrow \forall x\in A\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralrnmptw.1	$$⊢F=\left(x\in A⟼B\right)$$
2		ralrnmptw.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
3	1	fnmpt	$$⊢\forall x\in AB\in V\to FFnA$$
4		dfsbcq	$$⊢w=F\left(z\right)\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi \right)$$
5	4	ralrn	$$⊢FFnA\to \left(\forall w\in \mathrm{ran}F\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \forall z\in A\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi \right)$$
6	3 5	syl	$$⊢\forall x\in AB\in V\to \left(\forall w\in \mathrm{ran}F\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \forall z\in A\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi \right)$$
7		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
8		nfv	$$⊢Ⅎw\psi$$
9		sbceq2a	$$⊢w=y\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \psi \right)$$
10	7 8 9	cbvralw	$$⊢\forall w\in \mathrm{ran}F\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \forall y\in \mathrm{ran}F\psi$$
11		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
12	1 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
14	12 13	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
15		nfv	$$⊢Ⅎx\psi$$
16	14 15	nfsbcw	$$⊢Ⅎx\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi$$
17		nfv	$$⊢Ⅎz\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi$$
18		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
19	18	sbceq1d	$$⊢z=x\to \left(\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \right)$$
20	16 17 19	cbvralw	$$⊢\forall z\in A\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \forall x\in A\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi$$
21	6 10 20	3bitr3g	$$⊢\forall x\in AB\in V\to \left(\forall y\in \mathrm{ran}F\psi \leftrightarrow \forall x\in A\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \right)$$
22	1	fvmpt2	$$⊢\left(x\in A\wedge B\in V\right)\to F\left(x\right)=B$$
23	22	sbceq1d	$$⊢\left(x\in A\wedge B\in V\right)\to \left(\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \right)$$
24	2	sbcieg	$$⊢B\in V\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
25	24	adantl	$$⊢\left(x\in A\wedge B\in V\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
26	23 25	bitrd	$$⊢\left(x\in A\wedge B\in V\right)\to \left(\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
27	26	ralimiaa	$$⊢\forall x\in AB\in V\to \forall x\in A\left(\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
28		ralbi	$$⊢\forall x\in A\left(\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)\to \left(\forall x\in A\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \forall x\in A\chi \right)$$
29	27 28	syl	$$⊢\forall x\in AB\in V\to \left(\forall x\in A\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \forall x\in A\chi \right)$$
30	21 29	bitrd	$$⊢\forall x\in AB\in V\to \left(\forall y\in \mathrm{ran}F\psi \leftrightarrow \forall x\in A\chi \right)$$