Theorem rabnc

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

	Ref	Expression
Assertion	rabnc	$$⊢\left\{x\in A|\phi \right\}\cap \left\{x\in A|\neg \phi \right\}=\varnothing$$

Proof

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