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

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 4 5 syl ( 𝑦 = 𝑥 → ( 𝜑𝜓 ) )
7 6 2 bj-cbveximi ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 )
8 3 biimprd ( 𝑥 = 𝑦 → ( 𝜓𝜑 ) )
9 8 1 bj-cbveximi ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜑 )
10 7 9 impbii ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )