Theorem rexpssxrxp 11185

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.)

Assertion

Ref	Expression
rexpssxrxp	⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Proof of Theorem rexpssxrxp

Step	Hyp	Ref	Expression
1		ressxr 11184	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5636	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 699	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3885   × cxp 5619  ℝcr 11032  ℝ^*cxr 11173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-un 3890  df-ss 3902  df-opab 5138  df-xp 5627  df-xr 11178

This theorem is referenced by:  ltrelxr  11201  xrsdsre  24798  ovolfioo  25456  ovolficc  25457  ovolficcss  25458  ovollb  25468  ovolicc2  25511  ovolfs2  25560  uniiccdif  25567  uniioovol  25568  uniiccvol  25569  uniioombllem2  25572  uniioombllem3a  25573  uniioombllem3  25574  uniioombllem4  25575  uniioombllem5  25576  uniioombl  25578  dyadmbllem  25588  opnmbllem  25590  icoreresf  37729  icoreelrn  37738  relowlpssretop  37741  opnmbllem0  38038  mblfinlem1  38039  mblfinlem2  38040  voliooicof  46453  ovolval3  47104  ovolval4lem2  47107  ovolval5lem2  47110  ovolval5lem3  47111  ovnovollem1  47113  ovnovollem2  47114