Theorem ralrnmpt

Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ralrnmptw when possible. (Contributed by Mario Carneiro, 20-Aug-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ralrnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
	ralrnmpt.2	$$⊢y=B\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ralrnmpt	$$⊢\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		ralrnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2		ralrnmpt.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		nfv	$$⊢Ⅎw\psi$$
8		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
9		sbceq1a	$$⊢y=w\to \left(\psi \leftrightarrow \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \right)$$
10	7 8 9	cbvral	$$⊢\forall y\in \mathrm{ran}F\psi \leftrightarrow \forall w\in \mathrm{ran}F\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi$$
11	10	bicomi	$$⊢\forall w\in \mathrm{ran}F\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\psi \leftrightarrow \forall y\in \mathrm{ran}F\psi$$
12		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
13	1 12	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
15	13 14	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
16		nfv	$$⊢Ⅎx\psi$$
17	15 16	nfsbc	$$⊢Ⅎx\underset{\dot{}}{[}F\left(z\right)/y\underset{\dot{}}{]}\psi$$
18		nfv	$$⊢Ⅎz\underset{\dot{}}{[}F\left(x\right)/y\underset{\dot{}}{]}\psi$$
19		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
20	19	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)$$
21	17 18 20	cbvral	$$⊢\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$$
22	6 11 21	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)$$
23	1	fvmpt2	$$⊢\left(x\in A\wedge B\in V\right)\to F\left(x\right)=B$$
24	23	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)$$
25	2	sbcieg	$$⊢B\in V\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
26	25	adantl	$$⊢\left(x\in A\wedge B\in V\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
27	24 26	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)$$
28	27	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)$$
29		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)$$
30	28 29	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)$$
31	22 30	bitrd	$$⊢\forall x\in AB\in V\to \left(\forall y\in \mathrm{ran}F\psi \leftrightarrow \forall x\in A\chi \right)$$