Theorem rexpssxrxp 11154

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

Syntax hints:   ⊆ wss 3902   × cxp 5614  ℝcr 11002  ℝ^*cxr 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-opab 5154  df-xp 5622  df-xr 11147

This theorem is referenced by:  ltrelxr  11170  xrsdsre  24724  ovolfioo  25393  ovolficc  25394  ovolficcss  25395  ovollb  25405  ovolicc2  25448  ovolfs2  25497  uniiccdif  25504  uniioovol  25505  uniiccvol  25506  uniioombllem2  25509  uniioombllem3a  25510  uniioombllem3  25511  uniioombllem4  25512  uniioombllem5  25513  uniioombl  25515  dyadmbllem  25525  opnmbllem  25527  icoreresf  37385  icoreelrn  37394  relowlpssretop  37397  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  voliooicof  46033  ovolval3  46684  ovolval4lem2  46687  ovolval5lem2  46690  ovolval5lem3  46691  ovnovollem1  46693  ovnovollem2  46694