Metamath Proof Explorer

Theorem rr2sscn2

Description: The cartesian square of RR is a subset of the cartesian square of CC . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion rr2sscn2 
|- ( RR X. RR ) C_ ( CC X. CC )

Proof

Step Hyp Ref Expression
1 ax-resscn 
 |-  RR C_ CC
2 xpss12 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) )
3 1 1 2 mp2an 
 |-  ( RR X. RR ) C_ ( CC X. CC )