Theorem rexpssxrxp 10686

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

Syntax hints:   ⊆ wss 3936   × cxp 5553  ℝcr 10536  ℝ^*cxr 10674

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-opab 5129  df-xp 5561  df-xr 10679

This theorem is referenced by:  ltrelxr  10702  xrsdsre  23418  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovollb  24080  ovolicc2  24123  ovolfs2  24172  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  dyadmbllem  24200  opnmbllem  24202  icoreresf  34636  icoreelrn  34645  relowlpssretop  34648  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  voliooicof  42301  ovolval3  42949  ovolval4lem2  42952  ovolval5lem2  42955  ovolval5lem3  42956  ovnovollem1  42958  ovnovollem2  42959