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 ) = (/) )