Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Removing dependencies on ax-13 (and ax-11)
bj-cbv2v
Metamath Proof Explorer
Description: Version of cbv2 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-cbv2v.1
⊢ Ⅎ x φ
bj-cbv2v.2
⊢ Ⅎ y φ
bj-cbv2v.3
⊢ φ → Ⅎ y ψ
bj-cbv2v.4
⊢ φ → Ⅎ x χ
bj-cbv2v.5
⊢ φ → x = y → ψ ↔ χ
Assertion
bj-cbv2v
⊢ φ → ∀ x ψ ↔ ∀ y χ
Proof
Step
Hyp
Ref
Expression
1
bj-cbv2v.1
⊢ Ⅎ x φ
2
bj-cbv2v.2
⊢ Ⅎ y φ
3
bj-cbv2v.3
⊢ φ → Ⅎ y ψ
4
bj-cbv2v.4
⊢ φ → Ⅎ x χ
5
bj-cbv2v.5
⊢ φ → x = y → ψ ↔ χ
6
2
nf5ri
⊢ φ → ∀ y φ
7
1
nfal
⊢ Ⅎ x ∀ y φ
8
7
nf5ri
⊢ ∀ y φ → ∀ x ∀ y φ
9
6 8
syl
⊢ φ → ∀ x ∀ y φ
10
3
nf5rd
⊢ φ → ψ → ∀ y ψ
11
4
nf5rd
⊢ φ → χ → ∀ x χ
12
10 11 5
bj-cbv2hv
⊢ ∀ x ∀ y φ → ∀ x ψ ↔ ∀ y χ
13
9 12
syl
⊢ φ → ∀ x ψ ↔ ∀ y χ