Theorem rexpssxrxp 11189

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

Syntax hints:   ⊆ wss 3903   × cxp 5630  ℝcr 11037  ℝ^*cxr 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-opab 5163  df-xp 5638  df-xr 11182

This theorem is referenced by:  ltrelxr  11205  xrsdsre  24767  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovollb  25448  ovolicc2  25491  ovolfs2  25540  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  dyadmbllem  25568  opnmbllem  25570  icoreresf  37601  icoreelrn  37610  relowlpssretop  37613  opnmbllem0  37901  mblfinlem1  37902  mblfinlem2  37903  voliooicof  46348  ovolval3  46999  ovolval4lem2  47002  ovolval5lem2  47005  ovolval5lem3  47006  ovnovollem1  47008  ovnovollem2  47009