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		biidd	$$⊢y=x\to \left(\perp \leftrightarrow \perp \right)$$
2	1	eqabbw	$$⊢A=\left\{y|\perp \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \perp \right)$$
3	2	biimpi	$$⊢A=\left\{y|\perp \right\}\to \forall x\left(x\in A\leftrightarrow \perp \right)$$
4		nbfal	$$⊢\neg x\in A\leftrightarrow \left(x\in A\leftrightarrow \perp \right)$$
5		pm2.21	$$⊢\neg x\in A\to \left(x\in A\to \phi \right)$$
6	4 5	sylbir	$$⊢\left(x\in A\leftrightarrow \perp \right)\to \left(x\in A\to \phi \right)$$
7	3 6	sylg	$$⊢A=\left\{y|\perp \right\}\to \forall x\left(x\in A\to \phi \right)$$
8		dfnul4	$$⊢\varnothing =\left\{y|\perp \right\}$$
9	8	eqeq2i	$$⊢A=\varnothing \leftrightarrow A=\left\{y|\perp \right\}$$
10		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
11	7 9 10	3imtr4i	$$⊢A=\varnothing \to \forall x\in A\phi$$