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

Metamath Proof Explorer

Theorem raln

Description: Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021)

		Ref	Expression
	Assertion	raln	$⊢ \forall x \in A \neg φ \leftrightarrow \forall x \neg (x \in A \land φ)$

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall x \in A \neg φ \leftrightarrow \forall x (x \in A \to \neg φ)$
2		imnang	$⊢ \forall x (x \in A \to \neg φ) \leftrightarrow \forall x \neg (x \in A \land φ)$
3	1 2	bitri	$⊢ \forall x \in A \neg φ \leftrightarrow \forall x \neg (x \in A \land φ)$