Theorem cbvald

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]. See cbvaldw for a version with x , y disjoint, not depending on [ax-13]. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (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 (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)

Proof

nfv

cbvald.1

cbvald.2

nfvd

cbvald.3

cbv2 l0 l1 l2 l3 _