Theorem ec0

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

	Ref	Expression
Assertion	ec0	⊢ [ 𝐴 ] ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		df-ec	⊢ [ 𝐴 ] ∅ = ( ∅ “ { 𝐴 } )
2		0ima	⊢ ( ∅ “ { 𝐴 } ) = ∅
3	1 2	eqtri	⊢ [ 𝐴 ] ∅ = ∅