Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Removing dependencies on ax-13 (and ax-11)
bj-cbvaldv
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )