5
Use of this equality is often referred to as
α
-conversion.