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

Metamath Proof Explorer

Theorem rabeq0

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010) (Revised by BJ, 16-Jul-2021)

		Ref	Expression
	Assertion	rabeq0	$⊢ \{x \in A \| φ\} = \emptyset \leftrightarrow \forall x \in A \neg φ$

Step	Hyp	Ref	Expression
1		ab0	$⊢ \{x \| (x \in A \land φ)\} = \emptyset \leftrightarrow \forall x \neg (x \in A \land φ)$
2		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
3	2	eqeq1i	$⊢ \{x \in A \| φ\} = \emptyset \leftrightarrow \{x \| (x \in A \land φ)\} = \emptyset$
4		raln	$⊢ \forall x \in A \neg φ \leftrightarrow \forall x \neg (x \in A \land φ)$
5	1 3 4	3bitr4i	$⊢ \{x \in A \| φ\} = \emptyset \leftrightarrow \forall x \in A \neg φ$