Metamath Proof Explorer


Theorem cbvralw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvral with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 31-Jul-2003) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvralw.1 𝑦 𝜑
cbvralw.2 𝑥 𝜓
cbvralw.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvralw ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑦𝐴 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvralw.1 𝑦 𝜑
2 cbvralw.2 𝑥 𝜓
3 cbvralw.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
4 nfcv 𝑥 𝐴
5 nfcv 𝑦 𝐴
6 4 5 1 2 3 cbvralfw ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑦𝐴 𝜓 )