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)

	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		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	abeq2i	|- ( x e. `' (/) <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) )
9	4 8	mtbir	|- -. x e. `' (/)
10	9	nel0	|- `' (/) = (/)