Theorem rabnc

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

	Ref	Expression
Assertion	rabnc	|- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/)

Proof

Step	Hyp	Ref	Expression
1		inrab	|- ( { x e. A | ph } i^i { x e. A | -. ph } ) = { x e. A | ( ph /\ -. ph ) }
2		pm3.24	|- -. ( ph /\ -. ph )
3	2	rgenw	|- A. x e. A -. ( ph /\ -. ph )
4		rabeq0	|- ( { x e. A | ( ph /\ -. ph ) } = (/) <-> A. x e. A -. ( ph /\ -. ph ) )
5	3 4	mpbir	|- { x e. A | ( ph /\ -. ph ) } = (/)
6	1 5	eqtri	|- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/)