Theorem fvmptrab

Description: Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv , but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	fvmptrab.f	$$⊢F=\left(x\in V⟼\left\{y\in M|\phi \right\}\right)$$
	fvmptrab.r	$$⊢x=X\to \left(\phi \leftrightarrow \psi \right)$$
	fvmptrab.s	$$⊢x=X\to M=N$$
	fvmptrab.v	$$⊢X\in V\to N\in \mathrm{V}$$
	fvmptrab.n	$$⊢X\notin V\to N=\varnothing$$
Assertion	fvmptrab	$$⊢F\left(X\right)=\left\{y\in N|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		fvmptrab.f	$$⊢F=\left(x\in V⟼\left\{y\in M|\phi \right\}\right)$$
2		fvmptrab.r	$$⊢x=X\to \left(\phi \leftrightarrow \psi \right)$$
3		fvmptrab.s	$$⊢x=X\to M=N$$
4		fvmptrab.v	$$⊢X\in V\to N\in \mathrm{V}$$
5		fvmptrab.n	$$⊢X\notin V\to N=\varnothing$$
6	1	a1i	$$⊢X\in V\to F=\left(x\in V⟼\left\{y\in M|\phi \right\}\right)$$
7	3 2	rabeqbidv	$$⊢x=X\to \left\{y\in M|\phi \right\}=\left\{y\in N|\psi \right\}$$
8	7	adantl	$$⊢\left(X\in V\wedge x=X\right)\to \left\{y\in M|\phi \right\}=\left\{y\in N|\psi \right\}$$
9		id	$$⊢X\in V\to X\in V$$
10		eqid	$$⊢\left\{y\in N|\psi \right\}=\left\{y\in N|\psi \right\}$$
11	10 4	rabexd	$$⊢X\in V\to \left\{y\in N|\psi \right\}\in \mathrm{V}$$
12	6 8 9 11	fvmptd	$$⊢X\in V\to F\left(X\right)=\left\{y\in N|\psi \right\}$$
13	1	fvmptndm	$$⊢\neg X\in V\to F\left(X\right)=\varnothing$$
14		df-nel	$$⊢X\notin V\leftrightarrow \neg X\in V$$
15		rabeq	$$⊢N=\varnothing \to \left\{y\in N|\psi \right\}=\left\{y\in \varnothing |\psi \right\}$$
16		rab0	$$⊢\left\{y\in \varnothing |\psi \right\}=\varnothing$$
17	15 16	eqtr2di	$$⊢N=\varnothing \to \varnothing =\left\{y\in N|\psi \right\}$$
18	5 17	syl	$$⊢X\notin V\to \varnothing =\left\{y\in N|\psi \right\}$$
19	14 18	sylbir	$$⊢\neg X\in V\to \varnothing =\left\{y\in N|\psi \right\}$$
20	13 19	eqtrd	$$⊢\neg X\in V\to F\left(X\right)=\left\{y\in N|\psi \right\}$$
21	12 20	pm2.61i	$$⊢F\left(X\right)=\left\{y\in N|\psi \right\}$$