Description: A wff like that in this theorem will be known as an "alternating
congruence". A special symbol might be considered if more uses come up.
They have many of the same properties as normal congruences, starting with
reflexivity.

JonesMatijasevic uses "a ≡ ± b (mod c)" for this construction.
The disjunction of divisibility constraints seems to adequately capture
the concept, but it's rather verbose and somewhat inelegant. Use of an
explicit equivalence relation might also work. (Contributed by Stefan
O'Rear, 2-Oct-2014)