Theorem rexpssxrxp 11009

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

Step	Hyp	Ref	Expression
1		ressxr 11008	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5601	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 689	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3888   × cxp 5584  ℝcr 10859  ℝ^*cxr 10997

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-un 3893  df-in 3895  df-ss 3905  df-opab 5138  df-xp 5592  df-xr 11002

This theorem is referenced by:  ltrelxr  11025  xrsdsre  23962  ovolfioo  24620  ovolficc  24621  ovolficcss  24622  ovollb  24632  ovolicc2  24675  ovolfs2  24724  uniiccdif  24731  uniioovol  24732  uniiccvol  24733  uniioombllem2  24736  uniioombllem3a  24737  uniioombllem3  24738  uniioombllem4  24739  uniioombllem5  24740  uniioombl  24742  dyadmbllem  24752  opnmbllem  24754  icoreresf  35510  icoreelrn  35519  relowlpssretop  35522  opnmbllem0  35800  mblfinlem1  35801  mblfinlem2  35802  voliooicof  43497  ovolval3  44145  ovolval4lem2  44148  ovolval5lem2  44151  ovolval5lem3  44152  ovnovollem1  44154  ovnovollem2  44155