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

Theorem rexpssxrxp 10663
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
StepHypRef Expression
1 ressxr 10662 . 2 ℝ ⊆ ℝ*
2 xpss12 5543 . 2 ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
31, 1, 2mp2an 691 1 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wss 3910   × cxp 5526  cr 10513  *cxr 10651
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473  df-un 3915  df-in 3917  df-ss 3927  df-opab 5102  df-xp 5534  df-xr 10656
This theorem is referenced by:  ltrelxr  10679  xrsdsre  23394  ovolfioo  24050  ovolficc  24051  ovolficcss  24052  ovollb  24062  ovolicc2  24105  ovolfs2  24154  uniiccdif  24161  uniioovol  24162  uniiccvol  24163  uniioombllem2  24166  uniioombllem3a  24167  uniioombllem3  24168  uniioombllem4  24169  uniioombllem5  24170  uniioombl  24172  dyadmbllem  24182  opnmbllem  24184  icoreresf  34657  icoreelrn  34666  relowlpssretop  34669  opnmbllem0  34979  mblfinlem1  34980  mblfinlem2  34981  voliooicof  42461  ovolval3  43109  ovolval4lem2  43112  ovolval5lem2  43115  ovolval5lem3  43116  ovnovollem1  43118  ovnovollem2  43119
  Copyright terms: Public domain W3C validator