Theorem cbvexd
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim. Usage of this
theorem is discouraged because it depends on [ax-13]. Use the weaker
cbvexdw if possible. (Contributed by NM, 2-Jan-2002.) (Revised by
Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
Hypotheses
cbvald.1
\( \vdash \Finv y \, \varphi \)
cbvald.2
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbvald.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\exists x \, \psi \leftrightarrow \exists y \, \chi) \)
Proof
l0
cbvald.1
cbvald.2
l2
nfnd _
l3
cbvald.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
notbi
\( \vdash \psi \leftrightarrow \chi \leftrightarrow (\neg \psi \leftrightarrow \neg \chi) \)
imbitrdi l3 _
l6
cbvald l0 l2 _
\( \vdash \varphi \rightarrow (\forall x \, \neg \psi \leftrightarrow \forall y \, \neg \chi) \)
l7
alnex
\( \vdash \forall x \, \neg \psi \leftrightarrow \neg \exists x \, \psi \)
alnex
\( \vdash \forall y \, \neg \chi \leftrightarrow \neg \exists y \, \chi \)
3bitr3g l6 l7 _
con4bid _