Theorem rexpssxrxp 11255

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

Syntax hints:   ⊆ wss 3906   × cxp 5661  ℝcr 11100  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-opab 5175  df-xp 5669  df-xr 11248

This theorem is referenced by:  ltrelxr  11271  xrsdsre  24949  ovolfioo  25607  ovolficc  25608  ovolficcss  25609  ovollb  25619  ovolicc2  25662  ovolfs2  25711  uniiccdif  25718  uniioovol  25719  uniiccvol  25720  uniioombllem2  25723  uniioombllem3a  25724  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  uniioombl  25729  dyadmbllem  25739  opnmbllem  25741  icoreresf  37976  icoreelrn  37985  relowlpssretop  37988  opnmbllem0  38285  mblfinlem1  38286  mblfinlem2  38287  voliooicof  46690  ovolval3  47341  ovolval4lem2  47344  ovolval5lem2  47347  ovolval5lem3  47348  ovnovollem1  47350  ovnovollem2  47351