Derived propositional, quantifier and equality rules

The formulas $A\to A$, $A\to \mathrm{\neg }\mathrm{\neg }A$, $\mathrm{\neg }\mathrm{\neg }A\to A$, $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$, $A\to (B\to A\wedge B)$, $A\wedge B\to A$, $A\wedge B\to B$, and $A\to (\mathrm{\neg }A\to B)$ are Boolean tautologies, hence axioms. Applying MP to the displayed antecedents gives the asserted rules. Reflexivity gives $v_0=v_0$; generalization gives $\mathrm{\forall }{v}_0(v_0=v_0)$, which is literally $\mathrm{\neg }\mathrm{\perp }$ for $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$. From $\mathrm{\perp }$ and this theorem, the last tautology yields any formula. Conversely contradictory formulas yield $\mathrm{\perp }$ by the same tautology with $B=\mathrm{\perp }$.

Suppose $y$ occurs nowhere in $\varphi$. Instantiation gives $\mathrm{\forall }x\varphi \to \varphi [y\mathrm{/}x]$. Generalize $y$ and use restricted distribution, with $y$ absent from $\mathrm{\forall }x\varphi$, to obtain $\mathrm{\forall }x\varphi \to \mathrm{\forall }y\varphi [y\mathrm{/}x]$. Conversely instantiate $\mathrm{\forall }y\varphi [y\mathrm{/}x]$ at $x$. The substitution is free-for and returns $\varphi$: each new free $y$ is at an originally free $x$ position, hence below no $x$ binder. Generalizing $x$ and distributing gives the converse implication, since $x$ is not free in $\mathrm{\forall }y\varphi [y\mathrm{/}x]$.

Choose a variable $z$ absent from the displayed terms. Apply equality substitution to the formula $z=s$: $s=t\to (s=s\to t=s)$. Reflexivity and Boolean commutation of antecedents give $s=t\to t=s$. For transitivity use the formula $s=z$: $t=u\to (s=t\to s=u)$. MP gives $s=u$ from $s=t,t=u$. More generally the stated free-for formula substitution is already an axiom, and two MP applications give its inference; symmetry gives the reverse inference.

The axiom $\varphi [t\mathrm{/}x]\to \mathrm{\exists }x\varphi$ followed by MP proves existential introduction whenever $t$ is free for $x$. Given a proved $\varphi \to \psi$, combine it with the instance $\psi \to \mathrm{\exists }x\psi$ (substitution $x\mathrm{/}x$) using the Boolean composition tautology. This gives $\varphi \to \mathrm{\exists }x\psi$. Existential elimination now gives $\mathrm{\exists }x\varphi \to \mathrm{\exists }x\psi$, since $x$ is not free in its consequent. Apply this to each of $\mathrm{\neg }\mathrm{\neg }\varphi \to \varphi$ and $\varphi \to \mathrm{\neg }\mathrm{\neg }\varphi$ from step 1.1. The resulting two implications prove $\mathrm{\exists }x\mathrm{\neg }\mathrm{\neg }\varphi \leftrightarrow \mathrm{\exists }x\varphi$.

For existential renaming, introduction gives $\varphi [y\mathrm{/}x]\to \mathrm{\exists }x\varphi$; eliminate $y$, which is absent from the consequent. For the reverse direction introduction at $x$ gives $\varphi \to \mathrm{\exists }y\varphi [y\mathrm{/}x]$ by the same inverse-substitution calculation as step 1.2; eliminate $x$, which is absent from this consequent. Thus both renaming implications are theorems, including vacuous binders. No semantic equivalence has been substituted for a syntactic rule.