Metamath Proof Explorer

Theorem mptsuppdifd

Description: The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019)

Ref Expression
Hypotheses mptsuppdifd.f ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
mptsuppdifd.a ${⊢}{\phi }\to {A}\in {V}$
mptsuppdifd.z ${⊢}{\phi }\to {Z}\in {W}$
Assertion mptsuppdifd ${⊢}{\phi }\to {F}\mathrm{supp}{Z}=\left\{{x}\in {A}|{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$

Proof

Step Hyp Ref Expression
1 mptsuppdifd.f ${⊢}{F}=\left({x}\in {A}⟼{B}\right)$
2 mptsuppdifd.a ${⊢}{\phi }\to {A}\in {V}$
3 mptsuppdifd.z ${⊢}{\phi }\to {Z}\in {W}$
4 2 mptexd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
5 1 4 eqeltrid ${⊢}{\phi }\to {F}\in \mathrm{V}$
6 suppimacnv ${⊢}\left({F}\in \mathrm{V}\wedge {Z}\in {W}\right)\to {F}\mathrm{supp}{Z}={{F}}^{-1}\left[\mathrm{V}\setminus \left\{{Z}\right\}\right]$
7 5 3 6 syl2anc ${⊢}{\phi }\to {F}\mathrm{supp}{Z}={{F}}^{-1}\left[\mathrm{V}\setminus \left\{{Z}\right\}\right]$
8 1 mptpreima ${⊢}{{F}}^{-1}\left[\mathrm{V}\setminus \left\{{Z}\right\}\right]=\left\{{x}\in {A}|{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$
9 7 8 syl6eq ${⊢}{\phi }\to {F}\mathrm{supp}{Z}=\left\{{x}\in {A}|{B}\in \left(\mathrm{V}\setminus \left\{{Z}\right\}\right)\right\}$