Metamath Proof Explorer


Theorem rexpssxrxp

Description: The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion rexpssxrxp 2 * × *

Proof

Step Hyp Ref Expression
1 ressxr *
2 xpss12 * * 2 * × *
3 1 1 2 mp2an 2 * × *