Theorem rexpssxrxp 10408

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

Syntax hints:   ⊆ wss 3798   × cxp 5344  ℝcr 10258  ℝ^*cxr 10397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-in 3805  df-ss 3812  df-opab 4938  df-xp 5352  df-xr 10402

This theorem is referenced by:  ltrelxr  10425  xrsdsre  22990  ovolfioo  23640  ovolficc  23641  ovolficcss  23642  ovollb  23652  ovolicc2  23695  ovolfs2  23744  uniiccdif  23751  uniioovol  23752  uniiccvol  23753  uniioombllem2  23756  uniioombllem3a  23757  uniioombllem3  23758  uniioombllem4  23759  uniioombllem5  23760  uniioombl  23762  dyadmbllem  23772  opnmbllem  23774  icoreresf  33744  icoreelrn  33753  relowlpssretop  33756  opnmbllem0  33988  mblfinlem1  33989  mblfinlem2  33990  voliooicof  41005  ovolval3  41653  ovolval4lem2  41656  ovolval5lem2  41659  ovolval5lem3  41660  ovnovollem1  41662  ovnovollem2  41663