Definition 1.4.1.  Let S, T be sets. We define:
Rel(S, T) :=: {[ps,t]s ∈ S,t ∈ T | ps,t is a proposition for each s ∈ S and t ∈ T}
[ps,t]s ∈ S,t ∈ T = [qs,t]s ∈ S,t ∈ T  :⇔  ∀ s ∈ S, t ∈ T : [ps,t  ⇔  qs,t]  (ps,t is a proposition for each s ∈ S and t ∈ T, qs,t is a proposition for each s ∈ S and t ∈ T)
Prp(S × T) =: Rel(S, T) viar = [r((s, t))]s ∈ S,t ∈ T
Well-definedness.  No proof.
We write “let ≺ be a relation from S to T” for “let ≺ ∈ Rel(S, T).”
Remarks.

This definition encodes a relation from S to T as a proposition depending on an element of S and an element of T (up to equivalence). It would be equally possible to encode relations as subsets of the Cartesian product; the given definition is just more convenient.

References.