Theorem ec0

Description: The empty-coset of a class is the empty set. (Contributed by Peter Mazsa, 19-May-2019)

	Ref	Expression
Assertion	ec0	$$⊢\left[A\right]\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-ec	$$⊢\left[A\right]\varnothing =\varnothing \left[\left\{A\right\}\right]$$
2		0ima	$$⊢\varnothing \left[\left\{A\right\}\right]=\varnothing$$
3	1 2	eqtri	$$⊢\left[A\right]\varnothing =\varnothing$$