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

Metamath Proof Explorer

Theorem ralf0

Description: The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021)

		Ref	Expression
	Hypothesis	ralf0.1	$⊢ \neg φ$
	Assertion	ralf0	$⊢ \forall x \in A φ \leftrightarrow A = \emptyset$

Step	Hyp	Ref	Expression
1		ralf0.1	$⊢ \neg φ$
2		mtt	$⊢ \neg φ \to (\neg x \in A \leftrightarrow (x \in A \to φ))$
3	1 2	ax-mp	$⊢ \neg x \in A \leftrightarrow (x \in A \to φ)$
4	3	albii	$⊢ \forall x \neg x \in A \leftrightarrow \forall x (x \in A \to φ)$
5		eq0	$⊢ A = \emptyset \leftrightarrow \forall x \neg x \in A$
6		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
7	4 5 6	3bitr4ri	$⊢ \forall x \in A φ \leftrightarrow A = \emptyset$