Theorem 14 RP: For r a relation expression and provided x, y, z d.n.o.f. in r, x, y d.n.o.f. in P,

|-  ("z  | z Î r: P )     º     ("x,y | á x,yñ Î r: P [z : = áx,yñ] ) .

This result can be understood as change of dummy. The proof is suggested by the textbook's treatment of (8.22).

("x,y | á x,yñ Î r: P [z : = áx,yñ] ) = (9.2) for multiple quantification ("x,y | : á x,yñ Î rÞ P [z : = áx,yñ] ) = (8.14), z d.n.o.f. in á x,yñ ("x,y | : ("z | z = á x,yñ: z Î rÞ P ) ) = (9.4)(a) ("x,y | : ("z | z Î r: z = á x,yñÞ P ) ) = (8.19) for multiple quantification, x, y d.n.o.f. in z Î r ("z | z Î r: ("x,y  | : z = á x,yñÞ P ) ) = (9.2) for multiple quantification ("z | z Î r: ("x,y  | z = á x,yñ: P ) ) = (9.6) for multiple quantification, x, y d.n.o.f. in P ("z | z Î r: P  Ú  ("x,y  | : Ø (z = áx,yñ)) ) = (9.18) for multiple quantification ("z | z Î r: Ø($x,y  | : z = áx,yñ)  Ú  P ) = (3.59) ("z | z Î r: ($x,y  | : z = áx,yñ)  Þ  P ) = (9.4)(a) ("z | (z Î r)   Ù  ($x,y  | : z = áx,yñ):P ) = 14 R ("z | z Î r: P )

Theorem 14 RE: For r, t relation expressions and provided x, y d.n.o.f. in r or t,

|-  r = t       º       ("x,y|:áx,y ñ Î r   º áx,y ñ Î t) .

This is a straightforward proof by Mutual implication.
For necessity,

r = t      Þ      ("x,y | :áx,y ñ Î r   º áx,y ñ Î t) = (3.84)(b) r = t      Þ      ("x,y | :áx,y ñ Î r   º áx,y ñ Î r) = (3.3) r = t      Þ      ("x,y | :true) = (9.8) for multiple quantification r = t      Þ      true = (3.72) true .

Sufficiency follows using the Deduction Theorem.
Assume

("x,y|:áx,y ñ Î r   º áx,y ñ Î t) .

Let z be a fresh variable. We prove

z Î r     º     z Î t

from which

r   =   t .

z Î r = 14 R (z Î r)   Ù  ($x,y | :z = á x,yñ ) = (9.21) for multiple quantification ($x,y | :(z Î r)   Ù  z = á x,yñ ) = (3.84)(a) ($x,y | : á x,yñ Î r  Ù  z = á x,yñ ) = Assumption ($x,y | : á x,yñ Î t  Ù  z = á x,yñ ) = (3.84)(a) ($x,y | :(z Î t)   Ù  z = á x,yñ ) = (9.21) for multiple quantification (z Î t)   Ù  ($x,y | :z = á x,yñ ) = 14 R z Î t .