Metamath Proof Explorer


Theorem bj-cbvaldvav

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

Ref Expression
Hypothesis bj-cbvaldvav.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
Assertion bj-cbvaldvav ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )

Proof

Step Hyp Ref Expression
1 bj-cbvaldvav.1 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
2 nfv 𝑦 𝜑
3 nfvd ( 𝜑 → Ⅎ 𝑦 𝜓 )
4 1 ex ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
5 2 3 4 bj-cbvaldv ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )