Theorem rexpssxrxp 11181

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

Syntax hints:   ⊆ wss 3890   × cxp 5622  ℝcr 11028  ℝ^*cxr 11169

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 3432  df-un 3895  df-ss 3907  df-opab 5149  df-xp 5630  df-xr 11174

This theorem is referenced by:  ltrelxr  11197  xrsdsre  24786  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovollb  25456  ovolicc2  25499  ovolfs2  25548  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombl  25566  dyadmbllem  25576  opnmbllem  25578  icoreresf  37682  icoreelrn  37691  relowlpssretop  37694  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  voliooicof  46442  ovolval3  47093  ovolval4lem2  47096  ovolval5lem2  47099  ovolval5lem3  47100  ovnovollem1  47102  ovnovollem2  47103