Theorem falseral0

Description: A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020) (Proof shortened by TM, 16-Feb-2026)

	Ref	Expression
Assertion	falseral0	$$⊢\left(\forall x\neg \phi \wedge \forall x\in A\phi \right)\to A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		alral	$$⊢\forall x\neg \phi \to \forall x\in A\neg \phi$$
2		pm2.21	$$⊢\neg \phi \to \left(\phi \to \perp \right)$$
3	2	ral2imi	$$⊢\forall x\in A\neg \phi \to \left(\forall x\in A\phi \to \forall x\in A\perp \right)$$
4	3	imp	$$⊢\left(\forall x\in A\neg \phi \wedge \forall x\in A\phi \right)\to \forall x\in A\perp$$
5	1 4	sylan	$$⊢\left(\forall x\neg \phi \wedge \forall x\in A\phi \right)\to \forall x\in A\perp$$
6		fal	$$⊢\neg \perp$$
7	6	ralf0	$$⊢\forall x\in A\perp \leftrightarrow A=\varnothing$$
8	5 7	sylib	$$⊢\left(\forall x\neg \phi \wedge \forall x\in A\phi \right)\to A=\varnothing$$