Theorem rr2sscn2

Description: The cartesian square of RR is a subset of the cartesian square of CC . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	rr2sscn2	$$⊢{ℝ}^2\subseteq ℂ\times ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		xpss12	$$⊢\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^2\subseteq ℂ\times ℂ$$
3	1 1 2	mp2an	$$⊢{ℝ}^2\subseteq ℂ\times ℂ$$