Metamath Proof Explorer


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