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=\varnothing \to \forall x\in A\phi$$

Proof

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