Theorem rexpssxrxp 11309

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

Syntax hints:   ⊆ wss 3947   × cxp 5680  ℝcr 11157  ℝ^*cxr 11297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-ss 3964  df-opab 5216  df-xp 5688  df-xr 11302

This theorem is referenced by:  ltrelxr  11325  xrsdsre  24817  ovolfioo  25487  ovolficc  25488  ovolficcss  25489  ovollb  25499  ovolicc2  25542  ovolfs2  25591  uniiccdif  25598  uniioovol  25599  uniiccvol  25600  uniioombllem2  25603  uniioombllem3a  25604  uniioombllem3  25605  uniioombllem4  25606  uniioombllem5  25607  uniioombl  25609  dyadmbllem  25619  opnmbllem  25621  icoreresf  37059  icoreelrn  37068  relowlpssretop  37071  opnmbllem0  37357  mblfinlem1  37358  mblfinlem2  37359  voliooicof  45617  ovolval3  46268  ovolval4lem2  46271  ovolval5lem2  46274  ovolval5lem3  46275  ovnovollem1  46277  ovnovollem2  46278