Metamath Proof Explorer


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 { ∅ } = ∅