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 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
Assertion cbvraldva ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑦𝐴 𝜒 ) )

Proof

Step Hyp Ref Expression
1 cbvraldva.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
2 1 ancoms ( ( 𝑥 = 𝑦𝜑 ) → ( 𝜓𝜒 ) )
3 2 pm5.74da ( 𝑥 = 𝑦 → ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) )
4 3 cbvralvw ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ∀ 𝑦𝐴 ( 𝜑𝜒 ) )
5 r19.21v ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( 𝜑 → ∀ 𝑥𝐴 𝜓 ) )
6 r19.21v ( ∀ 𝑦𝐴 ( 𝜑𝜒 ) ↔ ( 𝜑 → ∀ 𝑦𝐴 𝜒 ) )
7 4 5 6 3bitr3i ( ( 𝜑 → ∀ 𝑥𝐴 𝜓 ) ↔ ( 𝜑 → ∀ 𝑦𝐴 𝜒 ) )
8 7 pm5.74ri ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑦𝐴 𝜒 ) )