This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbv1v

Description: Rule used to change bound variables, using implicit substitution. Version of cbv1 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by BJ, 16-Jun-2019)

Ref Expression
Hypotheses cbv1v.1 ⊢ Ⅎ x φ
cbv1v.2 ⊢ Ⅎ y φ
cbv1v.3 ⊢ φ → Ⅎ y ψ
cbv1v.4 ⊢ φ → Ⅎ x χ
cbv1v.5 ⊢ φ → x = y → ψ → χ
Assertion cbv1v ⊢ φ → ∀ x ψ → ∀ y χ

Proof

Step Hyp Ref Expression
1 cbv1v.1 ⊢ Ⅎ x φ
2 cbv1v.2 ⊢ Ⅎ y φ
3 cbv1v.3 ⊢ φ → Ⅎ y ψ
4 cbv1v.4 ⊢ φ → Ⅎ x χ
5 cbv1v.5 ⊢ φ → x = y → ψ → χ
6 2 3 nfim1 ⊢ Ⅎ y φ → ψ
7 1 4 nfim1 ⊢ Ⅎ x φ → χ
8 5 com12 ⊢ x = y → φ → ψ → χ
9 8 a2d ⊢ x = y → φ → ψ → φ → χ
10 6 7 9 cbv3v ⊢ ∀ x φ → ψ → ∀ y φ → χ
11 1 19.21 ⊢ ∀ x φ → ψ ↔ φ → ∀ x ψ
12 2 19.21 ⊢ ∀ y φ → χ ↔ φ → ∀ y χ
13 10 11 12 3imtr3i ⊢ φ → ∀ x ψ → φ → ∀ y χ
14 13 pm2.86i ⊢ φ → ∀ x ψ → ∀ y χ