This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (X \in V \land Z \in V) \to X supp Z = \emptyset$

Step	Hyp	Ref	Expression
1		df-supp	$⊢ supp = (x \in V, z \in V ⟼ \{i \in dom x \| x [\{i\}] \neq \{z\}\})$
2	1	mpondm0	$⊢ \neg (X \in V \land Z \in V) \to X supp Z = \emptyset$