Theorem cbvmow
Rule used to change bound variables, using implicit substitution.
Version of cbvmo with a disjoint variable condition, which does not
require [ax-10], [ax-13]. (Contributed by NM, 9-Mar-1995.) (Revised
by GG, 23-May-2024.)
Hypotheses
cbvmow.1
\( \vdash \Finv y \, \varphi \)
cbvmow.2
\( \vdash \Finv x \, \psi \)
cbvmow.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, \psi \)
Proof
l0
cbvmow.1
nfv
l2
nfim l0 _
l3
cbvmow.2
nfv
l5
nfim l3 _
l6
cbvmow.3
equequ1
imbi12d l6 _
cbvalv1 l2 l5 _
l10
exbii _
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l11
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
dfmo
\( \vdash \exists^\ast y \, \psi \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
3bitr4i l10 l11 _