Theorem rexpssxrxp 11261

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

Syntax hints:   ⊆ wss 3948   × cxp 5674  ℝcr 11111  ℝ^*cxr 11249

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-xr 11254

This theorem is referenced by:  ltrelxr  11277  xrsdsre  24333  ovolfioo  24991  ovolficc  24992  ovolficcss  24993  ovollb  25003  ovolicc2  25046  ovolfs2  25095  uniiccdif  25102  uniioovol  25103  uniiccvol  25104  uniioombllem2  25107  uniioombllem3a  25108  uniioombllem3  25109  uniioombllem4  25110  uniioombllem5  25111  uniioombl  25113  dyadmbllem  25123  opnmbllem  25125  icoreresf  36319  icoreelrn  36328  relowlpssretop  36331  opnmbllem0  36610  mblfinlem1  36611  mblfinlem2  36612  voliooicof  44791  ovolval3  45442  ovolval4lem2  45445  ovolval5lem2  45448  ovolval5lem3  45449  ovnovollem1  45451  ovnovollem2  45452