Theorem rexpssxrxp 11224

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

Syntax hints:   ⊆ wss 3904   × cxp 5643  ℝcr 11069  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-opab 5162  df-xp 5651  df-xr 11217

This theorem is referenced by:  ltrelxr  11240  xrsdsre  24851  ovolfioo  25509  ovolficc  25510  ovolficcss  25511  ovollb  25521  ovolicc2  25564  ovolfs2  25613  uniiccdif  25620  uniioovol  25621  uniiccvol  25622  uniioombllem2  25625  uniioombllem3a  25626  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  uniioombl  25631  dyadmbllem  25641  opnmbllem  25643  icoreresf  37810  icoreelrn  37819  relowlpssretop  37822  opnmbllem0  38119  mblfinlem1  38120  mblfinlem2  38121  voliooicof  46534  ovolval3  47185  ovolval4lem2  47188  ovolval5lem2  47191  ovolval5lem3  47192  ovnovollem1  47194  ovnovollem2  47195