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	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	⊢ ℝ ⊆ ℂ
2		xpss12	⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
3	1 1 2	mp2an	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )