Theorem rexpssxrxp 10084

Description: The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
rexpssxrxp	⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Proof of Theorem rexpssxrxp

Step	Hyp	Ref	Expression
1		ressxr 10083	. 2 ⊢ ℝ ⊆ ℝ*
2		xpss12 5225	. 2 ⊢ ((ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3	1, 1, 2	mp2an 708	1 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)

Syntax hints:   ⊆ wss 3574   × cxp 5112  ℝcr 9935  ℝ^*cxr 10073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120  df-xr 10078

This theorem is referenced by:  ltrelxr  10099  xrsdsre  22613  ovolfioo  23236  ovolficc  23237  ovolficcss  23238  ovollb  23247  ovolicc2  23290  ovolfs2  23339  uniiccdif  23346  uniioovol  23347  uniiccvol  23348  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  dyadmbllem  23367  opnmbllem  23369  icoreresf  33200  icoreelrn  33209  relowlpssretop  33212  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  voliooicof  40213  ovolval3  40861  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovnovollem1  40870  ovnovollem2  40871