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

Theorem rexpssxrxp 11205
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 11204 . 2 ℝ ⊆ ℝ*
2 xpss12 5649 . 2 ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
31, 1, 2mp2an 691 1 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wss 3911   × cxp 5632  cr 11055  *cxr 11193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-opab 5169  df-xp 5640  df-xr 11198
This theorem is referenced by:  ltrelxr  11221  xrsdsre  24189  ovolfioo  24847  ovolficc  24848  ovolficcss  24849  ovollb  24859  ovolicc2  24902  ovolfs2  24951  uniiccdif  24958  uniioovol  24959  uniiccvol  24960  uniioombllem2  24963  uniioombllem3a  24964  uniioombllem3  24965  uniioombllem4  24966  uniioombllem5  24967  uniioombl  24969  dyadmbllem  24979  opnmbllem  24981  icoreresf  35869  icoreelrn  35878  relowlpssretop  35881  opnmbllem0  36160  mblfinlem1  36161  mblfinlem2  36162  voliooicof  44323  ovolval3  44974  ovolval4lem2  44977  ovolval5lem2  44980  ovolval5lem3  44981  ovnovollem1  44983  ovnovollem2  44984
  Copyright terms: Public domain W3C validator