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	$$⊢{\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		df-opab	$$⊢\left\{⟨z,y⟩|y\varnothing z\right\}=\left\{x|\exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)\right\}$$
7	5 6	eqtri	$$⊢{\varnothing }^{-1}=\left\{x|\exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)\right\}$$
8	7	abeq2i	$$⊢x\in {\varnothing }^{-1}\leftrightarrow \exists z\exists y\left(x=⟨z,y⟩\wedge y\varnothing z\right)$$
9	4 8	mtbir	$$⊢\neg x\in {\varnothing }^{-1}$$
10	9	nel0	$$⊢{\varnothing }^{-1}=\varnothing$$