Theorem cbvalv1

Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require [ax-13]. See cbvalvw for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-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 \forall x \, \varphi \leftrightarrow \forall y \, \psi \)
Proof
l0
cbvalv1.nf1
l1
cbvalv1.nf2
cbvalv1.1
biimpd _
l4
cbv3v l0 l1 _
l5
cbvalv1.nf2
l6
cbvalv1.nf1
cbvalv1.1
biimprd _
equcoms _
cbv3v l5 l6 _
impbii l4 _