The standard way of constructing modular arithmetic in "upper level" [0] is to define it over equivalence classes. For instance, let a ~ b mod 4 be the expected equivalence relationship for mod-4 arithmetic.
Then, define [x] = {a | a~x} to be the set of all numbers which are congruent to x mod 4.
At this point, we define [x]+[y] = [x+y] (along with the other arithmetic operations which are defined similarly). Then, there is just a bit of work to prove that the above definition is actually well defined (since the representative element we pick from both of the [x] and [y] sets is arbitrary, we must show that [x+y] is the same set regardless of which x and y we choose).
This means that, when we write 17 = 1 (mod 4), we are really saying [17]_4 = [1]_4; where [x]_n is the mod-n equivalence class containing x. The equal sign is literal, the numbers are not.
This type of implicit injection is actually fairly common in algebra. It is how we can view, for example, 17 as a natural number, real number, complex number, and polynomial without explicitly mapping it each time.
[0] Eg. an introductory undergrad course in abstract algebra.
17 = 1 (mod 4)
but rather
17 ≅ 1 (mod 4)
i.e. "17 is congruent to 1 mod 4", not "equal", though congruency mod n is an equivalence relation.