From my understanding, sometimes in proofs we may 'let' a certain variable be equal to a mathematical object in question for ease of referring to it. Then later on in the conclusion we may substitute back in the object. However, does this not mean that the final conclusion rests on the initial assumption that the variable is equal to the object in question? Is this then not a proof of the conditional if variable x is equal to object y, then: whatever conclusion?
For example, in the proof of the derivative of ln(x) as shown here
In the first step they let
y=lnx
and in the final step they substitute back in lnx for y to get the conclusion here:
d(lnx)/dx=1/x
So back to my question: surely, the initial assumption that y=lnx is not needed for the final conclusion of the derivative of the ln(x) function, as it can be proven without that assumption, but in this method of proof is the statement y=lnx not an assumption which is needed in order to reach the conclusion? Also in the proof above is it not a proof of the conditional if y=lnx then d(ln(x))/dx=1/x? Which I know is ridiculous since the variable y doesn't even appear in the second part of that conditional. Is there any rule or methodology which states that trivial assumptions/variable definitions can be ignored or not considered to be sufficient conditions of the desired conclusion?
The inference is licensed by the Natural deduction rule of Existential elimination:
The argument runs as follows: we know that there is $\ln x$ [i.e. $\exists z \ (z=\ln x)$] and we use the assumption that $y=\ln x$ [this is: $φ[y/z]$] , where $y$ is a new variable, in order to derive further statements.
We derive the formula: $\dfrac d {dx} \ln x= \dfrac 1 x$, which has no occurrences of $y$ [this is: $ψ$].
The conclusion does not mention $y$ any more, and none of the other assumptions of the argument, except for $y = \ln x$, mentions it.
Thus our conclusion does not depends on the "specific nature" of $y$, but only on the "general fact" that we know that there is $\ln x$.