Theorem supp0prc

Description: The support of a class is empty if either the class or the "zero" is a proper class. (Contributed by AV, 28-May-2019)

	Ref	Expression
Assertion	supp0prc	$$⊢\neg \left(X\in \mathrm{V}\wedge Z\in \mathrm{V}\right)\to X\mathrm{supp}Z=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-supp	$$⊢\mathrm{supp}=\left(x\in \mathrm{V},z\in \mathrm{V}⟼\left\{i\in \mathrm{dom}x|x\left[\left\{i\right\}\right]\ne \left\{z\right\}\right\}\right)$$
2	1	mpondm0	$$⊢\neg \left(X\in \mathrm{V}\wedge Z\in \mathrm{V}\right)\to X\mathrm{supp}Z=\varnothing$$