This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnv0

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Avoid ax-12 . (Revised by TM, 31-Jan-2026)

Ref Expression
Assertion cnv0 
|- `' (/) = (/)

Proof

Step Hyp Ref Expression
1 br0 
 |-  -. y (/) z
2 1 intnan 
 |-  -. ( x = <. z , y >. /\ y (/) z )
3 2 nex 
 |-  -. E. y ( x = <. z , y >. /\ y (/) z )
4 3 nex 
 |-  -. E. z E. y ( x = <. z , y >. /\ y (/) z )
5 df-cnv 
 |-  `' (/) = { <. z , y >. | y (/) z }
6 5 eleq2i 
 |-  ( x e. `' (/) <-> x e. { <. z , y >. | y (/) z } )
7 elopabw 
 |-  ( x e. _V -> ( x e. { <. z , y >. | y (/) z } <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) ) )
8 7 elv 
 |-  ( x e. { <. z , y >. | y (/) z } <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) )
9 6 8 bitri 
 |-  ( x e. `' (/) <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) )
10 4 9 mtbir 
 |-  -. x e. `' (/)
11 10 nel0 
 |-  `' (/) = (/)