Theorem rexpssxrxp 11272

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

This proof depends on syntax axioms:   ⊆ wss 3908   × cxp 5664  ℝcr 11117  ℝ^*cxr 11260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-opab 5179  df-xp 5672  df-xr 11265

This theorem is used by:  ltrelxr  11288  xrsdsre  25005  ovolfioo  25663  ovolficc  25664  ovolficcss  25665  ovollb  25675  ovolicc2  25718  ovolfs2  25767  uniiccdif  25774  uniioovol  25775  uniiccvol  25776  uniioombllem2  25779  uniioombllem3a  25780  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  uniioombl  25785  dyadmbllem  25795  opnmbllem  25797  icoreresf  38039  icoreelrn  38048  relowlpssretop  38051  opnmbllem0  38348  mblfinlem1  38349  mblfinlem2  38350  voliooicof  46751  ovolval3  47402  ovolval4lem2  47405  ovolval5lem2  47408  ovolval5lem3  47409  ovnovollem1  47411  ovnovollem2  47412