Theorem rexpssxrxp 11177

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

Syntax hints:   ⊆ wss 3901   × cxp 5622  ℝcr 11025  ℝ^*cxr 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-opab 5161  df-xp 5630  df-xr 11170

This theorem is referenced by:  ltrelxr  11193  xrsdsre  24755  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovollb  25436  ovolicc2  25479  ovolfs2  25528  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  dyadmbllem  25556  opnmbllem  25558  icoreresf  37553  icoreelrn  37562  relowlpssretop  37565  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  voliooicof  46236  ovolval3  46887  ovolval4lem2  46890  ovolval5lem2  46893  ovolval5lem3  46894  ovnovollem1  46896  ovnovollem2  46897