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 -1 =

Proof

Step Hyp Ref Expression
1 dfdm4 dom = ran -1
2 dmsn0 dom =
3 1 2 eqtr3i ran -1 =
4 relcnv Rel -1
5 relrn0 Rel -1 -1 = ran -1 =
6 4 5 ax-mp -1 = ran -1 =
7 3 6 mpbir -1 =