Theorem rexpssxrxp 11225

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

Syntax hints:   ⊆ wss 3916   × cxp 5638  ℝcr 11073  ℝ^*cxr 11213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-ss 3933  df-opab 5172  df-xp 5646  df-xr 11218

This theorem is referenced by:  ltrelxr  11241  xrsdsre  24705  ovolfioo  25374  ovolficc  25375  ovolficcss  25376  ovollb  25386  ovolicc2  25429  ovolfs2  25478  uniiccdif  25485  uniioovol  25486  uniiccvol  25487  uniioombllem2  25490  uniioombllem3a  25491  uniioombllem3  25492  uniioombllem4  25493  uniioombllem5  25494  uniioombl  25496  dyadmbllem  25506  opnmbllem  25508  icoreresf  37335  icoreelrn  37344  relowlpssretop  37347  opnmbllem0  37645  mblfinlem1  37646  mblfinlem2  37647  voliooicof  45987  ovolval3  46638  ovolval4lem2  46641  ovolval5lem2  46644  ovolval5lem3  46645  ovnovollem1  46647  ovnovollem2  46648