Theorem cbveu

Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbveuw, cbveuvw when possible. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)

Hypotheses
cbveu.1
\( \vdash \Finv y \, \varphi \)
cbveu.2
\( \vdash \Finv x \, \psi \)
cbveu.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, \psi \)
Proof
cbveu.1
l1
sb8eu _
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, [ y / x ] \, \varphi \)
l2
cbveu.2
cbveu.3
sbie l2 _
eubii _
\( \vdash \exists{!} y \, [ y / x ] \, \varphi \leftrightarrow \exists{!} y \, \psi \)
bitri l1 _