MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexpssxrxp Structured version   Visualization version   GIF version

Theorem rexpssxrxp 10036
Description: The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
rexpssxrxp (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Proof of Theorem rexpssxrxp
StepHypRef Expression
1 ressxr 10035 . 2 ℝ ⊆ ℝ*
2 xpss12 5191 . 2 ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
31, 1, 2mp2an 707 1 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wss 3559   × cxp 5077  cr 9887  *cxr 10025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-un 3564  df-in 3566  df-ss 3573  df-opab 4679  df-xp 5085  df-xr 10030
This theorem is referenced by:  ltrelxr  10051  xrsdsre  22536  ovolfioo  23159  ovolficc  23160  ovolficcss  23161  ovollb  23170  ovolicc2  23213  ovolfs2  23262  uniiccdif  23269  uniioovol  23270  uniiccvol  23271  uniioombllem2  23274  uniioombllem3a  23275  uniioombllem3  23276  uniioombllem4  23277  uniioombllem5  23278  uniioombl  23280  dyadmbllem  23290  opnmbllem  23292  icoreresf  32867  icoreelrn  32876  relowlpssretop  32879  opnmbllem0  33112  mblfinlem1  33113  mblfinlem2  33114  voliooicof  39546  ovolval3  40194  ovolval4lem2  40197  ovolval5lem2  40200  ovolval5lem3  40201  ovnovollem1  40203  ovnovollem2  40204
  Copyright terms: Public domain W3C validator