Metamath Proof Explorer

Theorem ralnralall

Description: A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018)

		Ref	Expression
	Assertion	ralnralall	$⊢ A \neq \emptyset \to ((\forall x \in A φ \land \forall x \in A \neg φ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall x \in A (φ \land \neg φ) \leftrightarrow (\forall x \in A φ \land \forall x \in A \neg φ)$
2		pm3.24	$⊢ \neg (φ \land \neg φ)$
3	2	bifal	$⊢ (φ \land \neg φ) \leftrightarrow ⊥$
4	3	ralbii	$⊢ \forall x \in A (φ \land \neg φ) \leftrightarrow \forall x \in A ⊥$
5		r19.3rzv	$⊢ A \neq \emptyset \to (⊥ \leftrightarrow \forall x \in A ⊥)$
6		falim	$⊢ ⊥ \to ψ$
7	5 6	syl6bir	$⊢ A \neq \emptyset \to (\forall x \in A ⊥ \to ψ)$
8	4 7	biimtrid	$⊢ A \neq \emptyset \to (\forall x \in A (φ \land \neg φ) \to ψ)$
9	1 8	biimtrrid	$⊢ A \neq \emptyset \to ((\forall x \in A φ \land \forall x \in A \neg φ) \to ψ)$