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

Metamath Proof Explorer

Theorem rzal

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid df-clel , ax-8 . (Revised by GG, 2-Sep-2024)

		Ref	Expression
	Assertion	rzal	$⊢ A = \emptyset \to \forall x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		pm2.21	$⊢ \neg x \in A \to (x \in A \to φ)$
2	1	alimi	$⊢ \forall x \neg x \in A \to \forall x (x \in A \to φ)$
3		eq0	$⊢ A = \emptyset \leftrightarrow \forall x \neg x \in A$
4		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
5	2 3 4	3imtr4i	$⊢ A = \emptyset \to \forall x \in A φ$