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	$$⊢{\varnothing }^{-1}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		br0	$$⊢\neg y\varnothing z$$
2	1	intnan	$$⊢\neg \left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
3	2	nex	$$⊢\neg \exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
4	3	nex	$$⊢\neg \exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
5		df-cnv	$$⊢{\varnothing }^{-1}=\left\{⟨z,y⟩|y\varnothing z\right\}$$
6	5	eleq2i	$$⊢x\in {\varnothing }^{-1}\leftrightarrow x\in \left\{⟨z,y⟩|y\varnothing z\right\}$$
7		elopabw	$$⊢x\in \mathrm{V}\to \left(x\in \left\{⟨z,y⟩|y\varnothing z\right\}\leftrightarrow \exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)\right)$$
8	7	elv	$$⊢x\in \left\{⟨z,y⟩|y\varnothing z\right\}\leftrightarrow \exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
9	6 8	bitri	$$⊢x\in {\varnothing }^{-1}\leftrightarrow \exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
10	4 9	mtbir	$$⊢\neg x\in {\varnothing }^{-1}$$
11	10	nel0	$$⊢{\varnothing }^{-1}=\varnothing$$