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

Metamath Proof Explorer

Theorem bj-cbv2hv

Description: Version of cbv2h 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-cbv2hv.1 ⊢ φ → ψ → ∀ y ψ
bj-cbv2hv.2 ⊢ φ → χ → ∀ x χ
bj-cbv2hv.3 ⊢ φ → x = y → ψ ↔ χ
Assertion bj-cbv2hv ⊢ ∀ x ∀ y φ → ∀ x ψ ↔ ∀ y χ

Proof

Step Hyp Ref Expression
1 bj-cbv2hv.1 ⊢ φ → ψ → ∀ y ψ
2 bj-cbv2hv.2 ⊢ φ → χ → ∀ x χ
3 bj-cbv2hv.3 ⊢ φ → x = y → ψ ↔ χ
4 biimp ⊢ ψ ↔ χ → ψ → χ
5 3 4 syl6 ⊢ φ → x = y → ψ → χ
6 1 2 5 bj-cbv1hv ⊢ ∀ x ∀ y φ → ∀ x ψ → ∀ y χ
7 equcomi ⊢ y = x → x = y
8 biimpr ⊢ ψ ↔ χ → χ → ψ
9 7 3 8 syl56 ⊢ φ → y = x → χ → ψ
10 2 1 9 bj-cbv1hv ⊢ ∀ y ∀ x φ → ∀ y χ → ∀ x ψ
11 10 alcoms ⊢ ∀ x ∀ y φ → ∀ y χ → ∀ x ψ
12 6 11 impbid ⊢ ∀ x ∀ y φ → ∀ x ψ ↔ ∀ y χ