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 
 |-  `' { (/) } = (/)