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

Metamath Proof Explorer

Theorem bj-cbval

Description: Changing a bound variable (universal quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbval.denote ⊢ ∀ y ∃ x x = y
bj-cbval.denote2 ⊢ ∀ x ∃ y y = x
bj-cbval.maj ⊢ x = y → φ ↔ ψ
bj-cbval.equcomiv ⊢ y = x → x = y
Assertion bj-cbval ⊢ ∀ x φ ↔ ∀ y ψ

Proof

Step Hyp Ref Expression
1 bj-cbval.denote ⊢ ∀ y ∃ x x = y
2 bj-cbval.denote2 ⊢ ∀ x ∃ y y = x
3 bj-cbval.maj ⊢ x = y → φ ↔ ψ
4 bj-cbval.equcomiv ⊢ y = x → x = y
5 3 biimpd ⊢ x = y → φ → ψ
6 5 1 bj-cbvalimi ⊢ ∀ x φ → ∀ y ψ
7 3 biimprd ⊢ x = y → ψ → φ
8 4 7 syl ⊢ y = x → ψ → φ
9 8 2 bj-cbvalimi ⊢ ∀ y ψ → ∀ x φ
10 6 9 impbii ⊢ ∀ x φ ↔ ∀ y ψ