Metamath Proof Explorer


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