Theorem cnvsn0

Description: The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	cnvsn0	⊢ ◡ { ∅ } = ∅

Proof

Step	Hyp	Ref	Expression
1		dfdm4	⊢ dom { ∅ } = ran ◡ { ∅ }
2		dmsn0	⊢ dom { ∅ } = ∅
3	1 2	eqtr3i	⊢ ran ◡ { ∅ } = ∅
4		relcnv	⊢ Rel ◡ { ∅ }
5		relrn0	⊢ ( Rel ◡ { ∅ } → ( ◡ { ∅ } = ∅ ↔ ran ◡ { ∅ } = ∅ ) )
6	4 5	ax-mp	⊢ ( ◡ { ∅ } = ∅ ↔ ran ◡ { ∅ } = ∅ )
7	3 6	mpbir	⊢ ◡ { ∅ } = ∅