Theorem 0r

Description: The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	0r	⊢ 0R ∈ R

Proof

Step	Hyp	Ref	Expression
1		1pr	⊢ 1P ∈ P
2		opelxpi	⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ⟨ 1P , 1P ⟩ ∈ ( P × P ) )
3	1 1 2	mp2an	⊢ ⟨ 1P , 1P ⟩ ∈ ( P × P )
4		enrex	⊢ ~R ∈ V
5	4	ecelqsi	⊢ ( ⟨ 1P , 1P ⟩ ∈ ( P × P ) → [ ⟨ 1P , 1P ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
6	3 5	ax-mp	⊢ [ ⟨ 1P , 1P ⟩ ] ~R ∈ ( ( P × P ) / ~R )
7		df-0r	⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
8		df-nr	⊢ R = ( ( P × P ) / ~R )
9	6 7 8	3eltr4i	⊢ 0R ∈ R