Theorem rabnc

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

	Ref	Expression
Assertion	rabnc	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) = ∅

Proof

Step	Hyp	Ref	Expression
1		inrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜑 ) }
2		pm3.24	⊢ ¬ ( 𝜑 ∧ ¬ 𝜑 )
3	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝜑 ∧ ¬ 𝜑 )
4		rabeq0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜑 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝜑 ∧ ¬ 𝜑 ) )
5	3 4	mpbir	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∧ ¬ 𝜑 ) } = ∅
6	1 5	eqtri	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) = ∅