Theorem rexpssxrxp 11190

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

Syntax hints:   ⊆ wss 3889   × cxp 5629  ℝcr 11037  ℝ^*cxr 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-opab 5148  df-xp 5637  df-xr 11183

This theorem is referenced by:  ltrelxr  11206  xrsdsre  24776  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovollb  25446  ovolicc2  25489  ovolfs2  25538  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  dyadmbllem  25566  opnmbllem  25568  icoreresf  37668  icoreelrn  37677  relowlpssretop  37680  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  voliooicof  46424  ovolval3  47075  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovnovollem1  47084  ovnovollem2  47085