Theorem 0nsr

Description: The empty set is not a signed real. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	0nsr	⊢ ¬ ∅ ∈ R

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∅ = ∅
2		enrer	⊢ ~R Er ( P × P )
3		erdm	⊢ ( ~R Er ( P × P ) → dom ~R = ( P × P ) )
4	2 3	ax-mp	⊢ dom ~R = ( P × P )
5		elqsn0	⊢ ( ( dom ~R = ( P × P ) ∧ ∅ ∈ ( ( P × P ) / ~R ) ) → ∅ ≠ ∅ )
6	4 5	mpan	⊢ ( ∅ ∈ ( ( P × P ) / ~R ) → ∅ ≠ ∅ )
7		df-nr	⊢ R = ( ( P × P ) / ~R )
8	6 7	eleq2s	⊢ ( ∅ ∈ R → ∅ ≠ ∅ )
9	8	necon2bi	⊢ ( ∅ = ∅ → ¬ ∅ ∈ R )
10	1 9	ax-mp	⊢ ¬ ∅ ∈ R