Theorem rexpssxrxp 10675

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

Syntax hints:   ⊆ wss 3881   × cxp 5517  ℝcr 10525  ℝ^*cxr 10663

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525  df-xr 10668

This theorem is referenced by:  ltrelxr  10691  xrsdsre  23415  ovolfioo  24071  ovolficc  24072  ovolficcss  24073  ovollb  24083  ovolicc2  24126  ovolfs2  24175  uniiccdif  24182  uniioovol  24183  uniiccvol  24184  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombl  24193  dyadmbllem  24203  opnmbllem  24205  icoreresf  34769  icoreelrn  34778  relowlpssretop  34781  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  voliooicof  42638  ovolval3  43286  ovolval4lem2  43289  ovolval5lem2  43292  ovolval5lem3  43293  ovnovollem1  43295  ovnovollem2  43296