This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (\forall x \neg φ \land \forall x \in A φ) \to A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		alral	$⊢ \forall x \neg φ \to \forall x \in A \neg φ$
2		pm2.21	$⊢ \neg φ \to (φ \to ⊥)$
3	2	ral2imi	$⊢ \forall x \in A \neg φ \to (\forall x \in A φ \to \forall x \in A ⊥)$
4	3	imp	$⊢ (\forall x \in A \neg φ \land \forall x \in A φ) \to \forall x \in A ⊥$
5	1 4	sylan	$⊢ (\forall x \neg φ \land \forall x \in A φ) \to \forall x \in A ⊥$
6		fal	$⊢ \neg ⊥$
7	6	ralf0	$⊢ \forall x \in A ⊥ \leftrightarrow A = \emptyset$
8	5 7	sylib	$⊢ (\forall x \neg φ \land \forall x \in A φ) \to A = \emptyset$