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

Theorem rexpssxrxp 9650
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 9649 . 2  |-  RR  C_  RR*
2 xpss12 5114 . 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 3481    X. cxp 5003   RRcr 9503   RR*cxr 9639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486  df-in 3488  df-ss 3495  df-opab 4512  df-xp 5011  df-xr 9644
This theorem is referenced by:  ltrelxr  9660  xrsdsre  21183  ovolfioo  21747  ovolficc  21748  ovolficcss  21749  ovollb  21758  ovolicc2  21801  ovolfs2  21848  uniiccdif  21855  uniioovol  21856  uniiccvol  21857  uniioombllem2  21860  uniioombllem3a  21861  uniioombllem3  21862  uniioombllem4  21863  uniioombllem5  21864  uniioombl  21866  dyadmbllem  21876  opnmbllem  21878  opnmbllem0  29977  mblfinlem1  29978  mblfinlem2  29979
  Copyright terms: Public domain W3C validator