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χ

Proof

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χ