Theorem rexpssxrxp 10286

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

Syntax hints:   ⊆ wss 3723   × cxp 5247  ℝcr 10137  ℝ^*cxr 10275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-opab 4847  df-xp 5255  df-xr 10280

This theorem is referenced by:  ltrelxr  10301  xrsdsre  22833  ovolfioo  23455  ovolficc  23456  ovolficcss  23457  ovollb  23467  ovolicc2  23510  ovolfs2  23559  uniiccdif  23566  uniioovol  23567  uniiccvol  23568  uniioombllem2  23571  uniioombllem3a  23572  uniioombllem3  23573  uniioombllem4  23574  uniioombllem5  23575  uniioombl  23577  dyadmbllem  23587  opnmbllem  23589  icoreresf  33537  icoreelrn  33546  relowlpssretop  33549  opnmbllem0  33778  mblfinlem1  33779  mblfinlem2  33780  voliooicof  40730  ovolval3  41381  ovolval4lem2  41384  ovolval5lem2  41387  ovolval5lem3  41388  ovnovollem1  41390  ovnovollem2  41391