Metamath Proof Explorer

Theorem falseral0OLD

Description: Obsolete version of falseral0 as of 16-Feb-2026. (Contributed by AV, 30-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	falseral0OLD	$⊢ (\forall x \neg φ \land \forall x \in A φ) \to A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
2		19.26	$⊢ \forall x (\neg φ \land (x \in A \to φ)) \leftrightarrow (\forall x \neg φ \land \forall x (x \in A \to φ))$
3		con3	$⊢ (x \in A \to φ) \to (\neg φ \to \neg x \in A)$
4	3	impcom	$⊢ (\neg φ \land (x \in A \to φ)) \to \neg x \in A$
5	4	alimi	$⊢ \forall x (\neg φ \land (x \in A \to φ)) \to \forall x \neg x \in A$
6		alnex	$⊢ \forall x \neg x \in A \leftrightarrow \neg \exists x x \in A$
7	5 6	sylib	$⊢ \forall x (\neg φ \land (x \in A \to φ)) \to \neg \exists x x \in A$
8		notnotb	$⊢ A = \emptyset \leftrightarrow \neg \neg A = \emptyset$
9		neq0	$⊢ \neg A = \emptyset \leftrightarrow \exists x x \in A$
10	8 9	xchbinx	$⊢ A = \emptyset \leftrightarrow \neg \exists x x \in A$
11	7 10	sylibr	$⊢ \forall x (\neg φ \land (x \in A \to φ)) \to A = \emptyset$
12	2 11	sylbir	$⊢ (\forall x \neg φ \land \forall x (x \in A \to φ)) \to A = \emptyset$
13	1 12	sylan2b	$⊢ (\forall x \neg φ \land \forall x \in A φ) \to A = \emptyset$