Metamath Proof Explorer

Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014) Avoid ax-8 , df-clel . (Revised by Gino Giotto, 6-Sep-2024)

		Ref	Expression
	Hypothesis	eq0rdv.1	$⊢ φ \to \neg x \in A$
	Assertion	eq0rdv	$⊢ φ \to A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		eq0rdv.1	$⊢ φ \to \neg x \in A$
2	1	alrimiv	$⊢ φ \to \forall x \neg x \in A$
3		dfnul4	$⊢ \emptyset = \{y \| ⊥\}$
4	3	eqeq2i	$⊢ A = \emptyset \leftrightarrow A = \{y \| ⊥\}$
5		dfcleq	$⊢ A = \{y \| ⊥\} \leftrightarrow \forall x (x \in A \leftrightarrow x \in \{y \| ⊥\})$
6		df-clab	$⊢ x \in \{y \| ⊥\} \leftrightarrow [x/ y] ⊥$
7		sbv	$⊢ [x/ y] ⊥ \leftrightarrow ⊥$
8	6 7	bitri	$⊢ x \in \{y \| ⊥\} \leftrightarrow ⊥$
9	8	bibi2i	$⊢ (x \in A \leftrightarrow x \in \{y \| ⊥\}) \leftrightarrow (x \in A \leftrightarrow ⊥)$
10	9	albii	$⊢ \forall x (x \in A \leftrightarrow x \in \{y \| ⊥\}) \leftrightarrow \forall x (x \in A \leftrightarrow ⊥)$
11		nbfal	$⊢ \neg x \in A \leftrightarrow (x \in A \leftrightarrow ⊥)$
12	11	bicomi	$⊢ (x \in A \leftrightarrow ⊥) \leftrightarrow \neg x \in A$
13	12	albii	$⊢ \forall x (x \in A \leftrightarrow ⊥) \leftrightarrow \forall x \neg x \in A$
14	10 13	bitri	$⊢ \forall x (x \in A \leftrightarrow x \in \{y \| ⊥\}) \leftrightarrow \forall x \neg x \in A$
15	4 5 14	3bitrri	$⊢ \forall x \neg x \in A \leftrightarrow A = \emptyset$
16	2 15	sylib	$⊢ φ \to A = \emptyset$