Theorem cbvexv1

Rule used to change bound variables, using implicit substitution. Version of cbvex with a disjoint variable condition, which does not require [ax-13]. See cbvexvw for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses
cbvalv1.nf1
\( \vdash \Finv y \, \varphi \)
cbvalv1.nf2
\( \vdash \Finv x \, \psi \)
cbvalv1.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists y \, \psi \)
Proof
cbvalv1.nf1
l1
nfn _
cbvalv1.nf2
l3
nfn _
cbvalv1.1
notbid _
l6
cbvalv1 l1 l3 _
\( \vdash \forall x \, \neg \varphi \leftrightarrow \forall y \, \neg \psi \)
l7
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
alnex
\( \vdash \forall y \, \neg \psi \leftrightarrow \neg \exists y \, \psi \)
3bitr3i l6 l7 _
con4bii _