Theorem rexpssxrxp 11242

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

Syntax hints:   ⊆ wss 3907   × cxp 5650  ℝcr 11087  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-opab 5168  df-xp 5658  df-xr 11235

This theorem is referenced by:  ltrelxr  11258  xrsdsre  24929  ovolfioo  25587  ovolficc  25588  ovolficcss  25589  ovollb  25599  ovolicc2  25642  ovolfs2  25691  uniiccdif  25698  uniioovol  25699  uniiccvol  25700  uniioombllem2  25703  uniioombllem3a  25704  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  uniioombl  25709  dyadmbllem  25719  opnmbllem  25721  icoreresf  37858  icoreelrn  37867  relowlpssretop  37870  opnmbllem0  38167  mblfinlem1  38168  mblfinlem2  38169  voliooicof  46568  ovolval3  47219  ovolval4lem2  47222  ovolval5lem2  47225  ovolval5lem3  47226  ovnovollem1  47228  ovnovollem2  47229