Metamath Proof Explorer


Theorem supp0

Description: The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion supp0
|- ( Z e. W -> ( (/) supp Z ) = (/) )

Proof

Step Hyp Ref Expression
1 0ex
 |-  (/) e. _V
2 suppval
 |-  ( ( (/) e. _V /\ Z e. W ) -> ( (/) supp Z ) = { i e. dom (/) | ( (/) " { i } ) =/= { Z } } )
3 1 2 mpan
 |-  ( Z e. W -> ( (/) supp Z ) = { i e. dom (/) | ( (/) " { i } ) =/= { Z } } )
4 dm0
 |-  dom (/) = (/)
5 rabeq
 |-  ( dom (/) = (/) -> { i e. dom (/) | ( (/) " { i } ) =/= { Z } } = { i e. (/) | ( (/) " { i } ) =/= { Z } } )
6 4 5 mp1i
 |-  ( Z e. W -> { i e. dom (/) | ( (/) " { i } ) =/= { Z } } = { i e. (/) | ( (/) " { i } ) =/= { Z } } )
7 rab0
 |-  { i e. (/) | ( (/) " { i } ) =/= { Z } } = (/)
8 7 a1i
 |-  ( Z e. W -> { i e. (/) | ( (/) " { i } ) =/= { Z } } = (/) )
9 3 6 8 3eqtrd
 |-  ( Z e. W -> ( (/) supp Z ) = (/) )