Theorem rexpssxrxp 11306

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

Syntax hints:   ⊆ wss 3951   × cxp 5683  ℝcr 11154  ℝ^*cxr 11294

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-opab 5206  df-xp 5691  df-xr 11299

This theorem is referenced by:  ltrelxr  11322  xrsdsre  24832  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovollb  25514  ovolicc2  25557  ovolfs2  25606  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  dyadmbllem  25634  opnmbllem  25636  icoreresf  37353  icoreelrn  37362  relowlpssretop  37365  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  voliooicof  46011  ovolval3  46662  ovolval4lem2  46665  ovolval5lem2  46668  ovolval5lem3  46669  ovnovollem1  46671  ovnovollem2  46672