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 Gino Giotto, 2-Sep-2024)

	Ref	Expression
Assertion	rzal	$$⊢A=\varnothing \to \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢A=\left\{y|\perp \right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in \left\{y|\perp \right\}\right)$$
2	1	biimpi	$$⊢A=\left\{y|\perp \right\}\to \forall x\left(x\in A\leftrightarrow x\in \left\{y|\perp \right\}\right)$$
3		df-clab	$$⊢x\in \left\{y|\perp \right\}\leftrightarrow \left[x/y\right]\perp$$
4		sbv	$$⊢\left[x/y\right]\perp \leftrightarrow \perp$$
5	3 4	bitri	$$⊢x\in \left\{y|\perp \right\}\leftrightarrow \perp$$
6	5	bibi2i	$$⊢\left(x\in A\leftrightarrow x\in \left\{y|\perp \right\}\right)\leftrightarrow \left(x\in A\leftrightarrow \perp \right)$$
7		nbfal	$$⊢\neg x\in A\leftrightarrow \left(x\in A\leftrightarrow \perp \right)$$
8		pm2.21	$$⊢\neg x\in A\to \left(x\in A\to \phi \right)$$
9	7 8	sylbir	$$⊢\left(x\in A\leftrightarrow \perp \right)\to \left(x\in A\to \phi \right)$$
10	6 9	sylbi	$$⊢\left(x\in A\leftrightarrow x\in \left\{y|\perp \right\}\right)\to \left(x\in A\to \phi \right)$$
11	2 10	sylg	$$⊢A=\left\{y|\perp \right\}\to \forall x\left(x\in A\to \phi \right)$$
12		dfnul4	$$⊢\varnothing =\left\{y|\perp \right\}$$
13	12	eqeq2i	$$⊢A=\varnothing \leftrightarrow A=\left\{y|\perp \right\}$$
14		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
15	11 13 14	3imtr4i	$$⊢A=\varnothing \to \forall x\in A\phi$$