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 
|- ( -. ( X e. _V /\ Z e. _V ) -> ( X supp Z ) = (/) )

Proof

Step Hyp Ref Expression
1 df-supp 
 |-  supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
2 1 mpondm0 
 |-  ( -. ( X e. _V /\ Z e. _V ) -> ( X supp Z ) = (/) )