Theorem rexpssxrxp 10689

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

Syntax hints:   ⊆ wss 3939   × cxp 5556  ℝcr 10539  ℝ^*cxr 10677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944  df-in 3946  df-ss 3955  df-opab 5132  df-xp 5564  df-xr 10682

This theorem is referenced by:  ltrelxr  10705  xrsdsre  23421  ovolfioo  24071  ovolficc  24072  ovolficcss  24073  ovollb  24083  ovolicc2  24126  ovolfs2  24175  uniiccdif  24182  uniioovol  24183  uniiccvol  24184  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombl  24193  dyadmbllem  24203  opnmbllem  24205  icoreresf  34637  icoreelrn  34646  relowlpssretop  34649  opnmbllem0  34932  mblfinlem1  34933  mblfinlem2  34934  voliooicof  42288  ovolval3  42936  ovolval4lem2  42939  ovolval5lem2  42942  ovolval5lem3  42943  ovnovollem1  42945  ovnovollem2  42946