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

Metamath Proof Explorer

Theorem dfnul3

Description: Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004) (Proof shortened by BJ, 23-Sep-2024)

		Ref	Expression
	Assertion	dfnul3	$⊢ \emptyset = \{x \in A \| \neg x \in A\}$

Step	Hyp	Ref	Expression
1		fal	$⊢ \neg ⊥$
2		pm3.24	$⊢ \neg (x \in A \land \neg x \in A)$
3	1 2	2false	$⊢ ⊥ \leftrightarrow (x \in A \land \neg x \in A)$
4	3	abbii	$⊢ \{x \| ⊥\} = \{x \| (x \in A \land \neg x \in A)\}$
5		dfnul4	$⊢ \emptyset = \{x \| ⊥\}$
6		df-rab	$⊢ \{x \in A \| \neg x \in A\} = \{x \| (x \in A \land \neg x \in A)\}$
7	4 5 6	3eqtr4i	$⊢ \emptyset = \{x \in A \| \neg x \in A\}$