Theorem rexpssxrxp 9963

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	⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Proof of Theorem rexpssxrxp

Step	Hyp	Ref	Expression
1		ressxr 9962	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5148	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 704	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3540   × cxp 5036  ℝcr 9814  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-xr 9957

This theorem is referenced by:  ltrelxr  9978  xrsdsre  22421  ovolfioo  23043  ovolficc  23044  ovolficcss  23045  ovollb  23054  ovolicc2  23097  ovolfs2  23145  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  dyadmbllem  23173  opnmbllem  23175  icoreresf  32376  icoreelrn  32385  relowlpssretop  32388  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  voliooicof  38889  ovolval3  39537  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovnovollem1  39546  ovnovollem2  39547