Theorem rexpssxrxp 11335

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

This proof depends on syntax axioms:   ⊆ wss 3899   × cxp 5649  ℝcr 11180  ℝ^*cxr 11323

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-opab 5168  df-xp 5657  df-xr 11328

This theorem is used by:  ltrelxr  11351  xrsdsre  25110  ovolfioo  25768  ovolficc  25769  ovolficcss  25770  ovollb  25780  ovolicc2  25823  ovolfs2  25872  uniiccdif  25879  uniioovol  25880  uniiccvol  25881  uniioombllem2  25884  uniioombllem3a  25885  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  uniioombl  25890  dyadmbllem  25900  opnmbllem  25902  icoreresf  38243  icoreelrn  38252  relowlpssretop  38255  opnmbllem0  38542  mblfinlem1  38543  mblfinlem2  38544  voliooicof  46950  ovolval3  47601  ovolval4lem2  47604  ovolval5lem2  47607  ovolval5lem3  47608  ovnovollem1  47610  ovnovollem2  47611