Theorem rexpssxrxp 11304

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 11303	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5704	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 692	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3963   × cxp 5687  ℝcr 11152  ℝ^*cxr 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-opab 5211  df-xp 5695  df-xr 11297

This theorem is referenced by:  ltrelxr  11320  xrsdsre  24846  ovolfioo  25516  ovolficc  25517  ovolficcss  25518  ovollb  25528  ovolicc2  25571  ovolfs2  25620  uniiccdif  25627  uniioovol  25628  uniiccvol  25629  uniioombllem2  25632  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  uniioombllem5  25636  uniioombl  25638  dyadmbllem  25648  opnmbllem  25650  icoreresf  37335  icoreelrn  37344  relowlpssretop  37347  opnmbllem0  37643  mblfinlem1  37644  mblfinlem2  37645  voliooicof  45952  ovolval3  46603  ovolval4lem2  46606  ovolval5lem2  46609  ovolval5lem3  46610  ovnovollem1  46612  ovnovollem2  46613