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 ⊢ ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦
bj-cbval.denote2 ⊢ ∀ 𝑥 ∃ 𝑦 𝑦 = 𝑥
bj-cbval.maj ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
bj-cbval.equcomiv ⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
Assertion bj-cbval ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 bj-cbval.denote ⊢ ∀ 𝑦 ∃ 𝑥 𝑥 = 𝑦
2 bj-cbval.denote2 ⊢ ∀ 𝑥 ∃ 𝑦 𝑦 = 𝑥
3 bj-cbval.maj ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4 bj-cbval.equcomiv ⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
5 3 biimpd ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
6 5 1 bj-cbvalimi ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )
7 3 biimprd ⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
8 4 7 syl ⊢ ( 𝑦 = 𝑥 → ( 𝜓 → 𝜑 ) )
9 8 2 bj-cbvalimi ⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 )
10 6 9 impbii ⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )