Theorem rexpssxrxp 11179

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

Syntax hints:   ⊆ wss 3905   × cxp 5621  ℝcr 11027  ℝ^*cxr 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-opab 5158  df-xp 5629  df-xr 11172

This theorem is referenced by:  ltrelxr  11195  xrsdsre  24715  ovolfioo  25384  ovolficc  25385  ovolficcss  25386  ovollb  25396  ovolicc2  25439  ovolfs2  25488  uniiccdif  25495  uniioovol  25496  uniiccvol  25497  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombl  25506  dyadmbllem  25516  opnmbllem  25518  icoreresf  37325  icoreelrn  37334  relowlpssretop  37337  opnmbllem0  37635  mblfinlem1  37636  mblfinlem2  37637  voliooicof  45978  ovolval3  46629  ovolval4lem2  46632  ovolval5lem2  46635  ovolval5lem3  46636  ovnovollem1  46638  ovnovollem2  46639