Theorem rexpssxrxp 11020

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 11019	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5604	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 689	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3887   × cxp 5587  ℝcr 10870  ℝ^*cxr 11008

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 3434  df-un 3892  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-xr 11013

This theorem is referenced by:  ltrelxr  11036  xrsdsre  23973  ovolfioo  24631  ovolficc  24632  ovolficcss  24633  ovollb  24643  ovolicc2  24686  ovolfs2  24735  uniiccdif  24742  uniioovol  24743  uniiccvol  24744  uniioombllem2  24747  uniioombllem3a  24748  uniioombllem3  24749  uniioombllem4  24750  uniioombllem5  24751  uniioombl  24753  dyadmbllem  24763  opnmbllem  24765  icoreresf  35523  icoreelrn  35532  relowlpssretop  35535  opnmbllem0  35813  mblfinlem1  35814  mblfinlem2  35815  voliooicof  43537  ovolval3  44185  ovolval4lem2  44188  ovolval5lem2  44191  ovolval5lem3  44192  ovnovollem1  44194  ovnovollem2  44195