Theorem rexpssxrxp 11219

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

Syntax hints:   ⊆ wss 3914   × cxp 5636  ℝcr 11067  ℝ^*cxr 11207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-opab 5170  df-xp 5644  df-xr 11212

This theorem is referenced by:  ltrelxr  11235  xrsdsre  24699  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovollb  25380  ovolicc2  25423  ovolfs2  25472  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  dyadmbllem  25500  opnmbllem  25502  icoreresf  37340  icoreelrn  37349  relowlpssretop  37352  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  voliooicof  45994  ovolval3  46645  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovnovollem1  46654  ovnovollem2  46655