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

Theorem rexpssxrxp 9428
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  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )

Proof of Theorem rexpssxrxp
StepHypRef Expression
1 ressxr 9427 . 2  |-  RR  C_  RR*
2 xpss12 4945 . 2  |-  ( ( RR  C_  RR*  /\  RR  C_ 
RR* )  ->  ( RR  X.  RR )  C_  ( RR*  X.  RR* )
)
31, 1, 2mp2an 672 1  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3328    X. cxp 4838   RRcr 9281   RR*cxr 9417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-in 3335  df-ss 3342  df-opab 4351  df-xp 4846  df-xr 9422
This theorem is referenced by:  ltrelxr  9438  xrsdsre  20387  ovolfioo  20951  ovolficc  20952  ovolficcss  20953  ovollb  20962  ovolicc2  21005  ovolfs2  21051  uniiccdif  21058  uniioovol  21059  uniiccvol  21060  uniioombllem2  21063  uniioombllem3a  21064  uniioombllem3  21065  uniioombllem4  21066  uniioombllem5  21067  uniioombl  21069  dyadmbllem  21079  opnmbllem  21081  opnmbllem0  28427  mblfinlem1  28428  mblfinlem2  28429
  Copyright terms: Public domain W3C validator