Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steve Rodriguez
Miscellanea
ssrecnpr
Next ⟩
seff
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssrecnpr
Description:
RR
is a subset of both
RR
and
CC
.
(Contributed by
Steve Rodriguez
, 22-Nov-2015)
Ref
Expression
Assertion
ssrecnpr
⊢
S
∈
ℝ
ℂ
→
ℝ
⊆
S
Proof
Step
Hyp
Ref
Expression
1
elpri
⊢
S
∈
ℝ
ℂ
→
S
=
ℝ
∨
S
=
ℂ
2
eqimss2
⊢
S
=
ℝ
→
ℝ
⊆
S
3
ax-resscn
⊢
ℝ
⊆
ℂ
4
sseq2
⊢
S
=
ℂ
→
ℝ
⊆
S
↔
ℝ
⊆
ℂ
5
3
4
mpbiri
⊢
S
=
ℂ
→
ℝ
⊆
S
6
2
5
jaoi
⊢
S
=
ℝ
∨
S
=
ℂ
→
ℝ
⊆
S
7
1
6
syl
⊢
S
∈
ℝ
ℂ
→
ℝ
⊆
S