Metamath Proof Explorer

Theorem cbvexdva

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

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


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