Theorem rexpssxrxp 11226

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

Syntax hints:   ⊆ wss 3917   × cxp 5639  ℝcr 11074  ℝ^*cxr 11214

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-opab 5173  df-xp 5647  df-xr 11219

This theorem is referenced by:  ltrelxr  11242  xrsdsre  24706  ovolfioo  25375  ovolficc  25376  ovolficcss  25377  ovollb  25387  ovolicc2  25430  ovolfs2  25479  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  dyadmbllem  25507  opnmbllem  25509  icoreresf  37347  icoreelrn  37356  relowlpssretop  37359  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  voliooicof  46001  ovolval3  46652  ovolval4lem2  46655  ovolval5lem2  46658  ovolval5lem3  46659  ovnovollem1  46661  ovnovollem2  46662