Theorem rexpssxrxp 10951

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

Syntax hints:   ⊆ wss 3883   × cxp 5578  ℝcr 10801  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-xr 10944

This theorem is referenced by:  ltrelxr  10967  xrsdsre  23879  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovollb  24548  ovolicc2  24591  ovolfs2  24640  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  uniioombl  24658  dyadmbllem  24668  opnmbllem  24670  icoreresf  35450  icoreelrn  35459  relowlpssretop  35462  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  voliooicof  43427  ovolval3  44075  ovolval4lem2  44078  ovolval5lem2  44081  ovolval5lem3  44082  ovnovollem1  44084  ovnovollem2  44085