Theorem rexpssxrxp 11188

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

Syntax hints:   ⊆ wss 3890   × cxp 5623  ℝcr 11035  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-opab 5142  df-xp 5631  df-xr 11181

This theorem is referenced by:  ltrelxr  11204  xrsdsre  24801  ovolfioo  25459  ovolficc  25460  ovolficcss  25461  ovollb  25471  ovolicc2  25514  ovolfs2  25563  uniiccdif  25570  uniioovol  25571  uniiccvol  25572  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  uniioombl  25581  dyadmbllem  25591  opnmbllem  25593  icoreresf  37721  icoreelrn  37730  relowlpssretop  37733  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  voliooicof  46446  ovolval3  47097  ovolval4lem2  47100  ovolval5lem2  47103  ovolval5lem3  47104  ovnovollem1  47106  ovnovollem2  47107