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