# Metamath Proof Explorer

## 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 }↔{\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 }↔{\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 ${⊢}¬{X}\in {V}\to {F}\left({X}\right)=\varnothing$
14 df-nel ${⊢}{X}\notin {V}↔¬{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 syl6req ${⊢}{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 ${⊢}¬{X}\in {V}\to \varnothing =\left\{{y}\in {N}|{\psi }\right\}$
20 13 19 eqtrd ${⊢}¬{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\}$