Definition 2.1.1.6.  Let X, Y be sets, φ:X ↔ Y be a bijection,  be a relation on X,  be a relation on Y. We define
φ
by:
[px1,x2]x1,x2 ∈ Xφ[qy1,y2]y1,y2 ∈ Y  :⇔  ∀ x1, x2 ∈ X : [px1,x2  ⇔  qφ(x1),φ(x2)]  (qy1,y2 is a proposition for each y1, y2 ∈ Y, px1,x2 is a proposition for each x1, x2 ∈ X)  ⇔  ∀ x1, x2 ∈ X : [x1x2  ⇔  φ(x1) φ(x2)]
Equivalence.  No proof.