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

Metamath Proof Explorer

Theorem bj-cbvex

Description: Changing a bound variable (existential 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-cbvex ⊢ ∃ 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 4 5 syl ⊢ y = x → φ → ψ
7 6 2 bj-cbveximi ⊢ ∃ x φ → ∃ y ψ
8 3 biimprd ⊢ x = y → ψ → φ
9 8 1 bj-cbveximi ⊢ ∃ y ψ → ∃ x φ
10 7 9 impbii ⊢ ∃ x φ ↔ ∃ y ψ