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

Metamath Proof Explorer

Theorem cnv0OLD

Description: Obsolete version of cnv0 as of 31-Jan-2026. (Contributed by NM, 6-Apr-1998) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

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 df-opab 
 |-  { <. z , y >. | y (/) z } = { x | E. z E. y ( x = <. z , y >. /\ y (/) z ) }
7 5 6 eqtri 
 |-  `' (/) = { x | E. z E. y ( x = <. z , y >. /\ y (/) z ) }
8 7 eqabri 
 |-  ( x e. `' (/) <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) )
9 4 8 mtbir 
 |-  -. x e. `' (/)
10 9 nel0 
 |-  `' (/) = (/)