Metamath Proof Explorer


Theorem cbvaldva

Description: Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvaldvaw if possible. (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

Ref Expression
Hypothesis cbvaldva.1 φ x = y ψ χ
Assertion cbvaldva φ x ψ y χ

Proof

Step Hyp Ref Expression
1 cbvaldva.1 φ x = y ψ χ
2 nfv y φ
3 nfvd φ y ψ
4 1 ex φ x = y ψ χ
5 2 3 4 cbvald φ x ψ y χ