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

Metamath Proof Explorer

Theorem rabnc

Description: Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011)

		Ref	Expression
	Assertion	rabnc	$⊢ \{x \in A \| φ\} \cap \{x \in A \| \neg φ\} = \emptyset$

Step	Hyp	Ref	Expression
1		inrab	$⊢ \{x \in A \| φ\} \cap \{x \in A \| \neg φ\} = \{x \in A \| (φ \land \neg φ)\}$
2		pm3.24	$⊢ \neg (φ \land \neg φ)$
3	2	rgenw	$⊢ \forall x \in A \neg (φ \land \neg φ)$
4		rabeq0	$⊢ \{x \in A \| (φ \land \neg φ)\} = \emptyset \leftrightarrow \forall x \in A \neg (φ \land \neg φ)$
5	3 4	mpbir	$⊢ \{x \in A \| (φ \land \neg φ)\} = \emptyset$
6	1 5	eqtri	$⊢ \{x \in A \| φ\} \cap \{x \in A \| \neg φ\} = \emptyset$