Theorem rexpssxrxp 11335

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

Syntax hints:   ⊆ wss 3976   × cxp 5698  ℝcr 11183  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-opab 5229  df-xp 5706  df-xr 11328

This theorem is referenced by:  ltrelxr  11351  xrsdsre  24851  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovollb  25533  ovolicc2  25576  ovolfs2  25625  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombl  25643  dyadmbllem  25653  opnmbllem  25655  icoreresf  37318  icoreelrn  37327  relowlpssretop  37330  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  voliooicof  45917  ovolval3  46568  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovnovollem1  46577  ovnovollem2  46578