Metamath Proof Explorer

Theorem cbvriotavw

Description: Change bound variable in a restricted description binder. Version of cbvriotav with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Mar-2013) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypothesis cbvriotavw.1 x = y φ ψ
Assertion cbvriotavw ι x A | φ = ι y A | ψ


Step Hyp Ref Expression
1 cbvriotavw.1 x = y φ ψ
2 nfv y φ
3 nfv x ψ
4 2 3 1 cbvriotaw ι x A | φ = ι y A | ψ