Metamath Proof Explorer

Theorem recnprss

Description: Both RR and CC are subsets of CC . (Contributed by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion recnprss 
|- ( S e. { RR , CC } -> S C_ CC )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
2 ax-resscn 
 |-  RR C_ CC
3 sseq1 
 |-  ( S = RR -> ( S C_ CC <-> RR C_ CC ) )
4 2 3 mpbiri 
 |-  ( S = RR -> S C_ CC )
5 eqimss 
 |-  ( S = CC -> S C_ CC )
6 4 5 jaoi 
 |-  ( ( S = RR \/ S = CC ) -> S C_ CC )
7 1 6 syl 
 |-  ( S e. { RR , CC } -> S C_ CC )