Theorem rexpssxrxp 11282

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

This proof depends on syntax axioms:   ⊆ wss 3902   × cxp 5657  ℝcr 11127  ℝ^*cxr 11270

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-opab 5172  df-xp 5665  df-xr 11275

This theorem is used by:  ltrelxr  11298  xrsdsre  25043  ovolfioo  25701  ovolficc  25702  ovolficcss  25703  ovollb  25713  ovolicc2  25756  ovolfs2  25805  uniiccdif  25812  uniioovol  25813  uniiccvol  25814  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  uniioombl  25823  dyadmbllem  25833  opnmbllem  25835  icoreresf  38114  icoreelrn  38123  relowlpssretop  38126  opnmbllem0  38413  mblfinlem1  38414  mblfinlem2  38415  voliooicof  46832  ovolval3  47483  ovolval4lem2  47486  ovolval5lem2  47489  ovolval5lem3  47490  ovnovollem1  47492  ovnovollem2  47493