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 \phi$$
Assertion	ralf0	$$⊢\forall x\in A\phi \leftrightarrow A=\varnothing$$

Proof

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