Metamath Proof Explorer

Theorem cbvaldvaw

Description: Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017) (Revised by Gino Giotto, 10-Jan-2024) Reduce axiom usage, along an idea of Gino Giotto. (Revised by Wolf Lammen, 10-Feb-2024)

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


Step Hyp Ref Expression
1 cbvaldvaw.1 φ x = y ψ χ
2 1 ancoms x = y φ ψ χ
3 2 pm5.74da x = y φ ψ φ χ
4 3 cbvalvw x φ ψ y φ χ
5 19.21v x φ ψ φ x ψ
6 19.21v y φ χ φ y χ
7 4 5 6 3bitr3i φ x ψ φ y χ
8 7 pm5.74ri φ x ψ y χ