Theorem 1sr

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

	Ref	Expression
Assertion	1sr	⊢ 1R ∈ R

Proof

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