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	eqtrdi	$$⊢\phi \to F\mathrm{supp}Z=\left\{x\in A|B\in \left(\mathrm{V}\setminus \left\{Z\right\}\right)\right\}$$