Metamath Proof Explorer


Theorem bj-cbvaldv

Description: Version of cbvald with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbvaldv.1 𝑦 𝜑
bj-cbvaldv.2 ( 𝜑 → Ⅎ 𝑦 𝜓 )
bj-cbvaldv.3 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
Assertion bj-cbvaldv ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )

Proof

Step Hyp Ref Expression
1 bj-cbvaldv.1 𝑦 𝜑
2 bj-cbvaldv.2 ( 𝜑 → Ⅎ 𝑦 𝜓 )
3 bj-cbvaldv.3 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
4 nfv 𝑥 𝜑
5 nfv 𝑥 𝜒
6 5 a1i ( 𝜑 → Ⅎ 𝑥 𝜒 )
7 4 1 2 6 3 bj-cbv2v ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )