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

Metamath Proof Explorer

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

Proof

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