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	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑍 ∈ V ) → ( 𝑋 supp 𝑍 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-supp	⊢ supp = ( 𝑥 ∈ V , 𝑧 ∈ V ↦ { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } )
2	1	mpondm0	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑍 ∈ V ) → ( 𝑋 supp 𝑍 ) = ∅ )