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 e. { RR , CC } -> RR C_ S )

Proof

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