Theorem rexpssxrxp 11258

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

Syntax hints:   ⊆ wss 3948   × cxp 5674  ℝcr 11108  ℝ^*cxr 11246

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 11251

This theorem is referenced by:  ltrelxr  11274  xrsdsre  24325  ovolfioo  24983  ovolficc  24984  ovolficcss  24985  ovollb  24995  ovolicc2  25038  ovolfs2  25087  uniiccdif  25094  uniioovol  25095  uniiccvol  25096  uniioombllem2  25099  uniioombllem3a  25100  uniioombllem3  25101  uniioombllem4  25102  uniioombllem5  25103  uniioombl  25105  dyadmbllem  25115  opnmbllem  25117  icoreresf  36228  icoreelrn  36237  relowlpssretop  36240  opnmbllem0  36519  mblfinlem1  36520  mblfinlem2  36521  voliooicof  44702  ovolval3  45353  ovolval4lem2  45356  ovolval5lem2  45359  ovolval5lem3  45360  ovnovollem1  45362  ovnovollem2  45363