Metamath Proof Explorer


Theorem cbvraldva

Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 9-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 cbvraldva.1 φ x = y ψ χ
2 1 ancoms x = y φ ψ χ
3 2 pm5.74da x = y φ ψ φ χ
4 3 cbvralvw x A φ ψ y A φ χ
5 r19.21v x A φ ψ φ x A ψ
6 r19.21v y A φ χ φ y A χ
7 4 5 6 3bitr3i φ x A ψ φ y A χ
8 7 pm5.74ri φ x A ψ y A χ