Theorem rexpssxrxp 11164

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

Syntax hints:   ⊆ wss 3898   × cxp 5617  ℝcr 11012  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-opab 5156  df-xp 5625  df-xr 11157

This theorem is referenced by:  ltrelxr  11180  xrsdsre  24727  ovolfioo  25396  ovolficc  25397  ovolficcss  25398  ovollb  25408  ovolicc2  25451  ovolfs2  25500  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombl  25518  dyadmbllem  25528  opnmbllem  25530  icoreresf  37417  icoreelrn  37426  relowlpssretop  37429  opnmbllem0  37716  mblfinlem1  37717  mblfinlem2  37718  voliooicof  46118  ovolval3  46769  ovolval4lem2  46772  ovolval5lem2  46775  ovolval5lem3  46776  ovnovollem1  46778  ovnovollem2  46779