Theorem bj-cbvex

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

	Ref	Expression
Hypotheses	bj-cbval.denote	$$⊢\forall y\exists xx=y$$
	bj-cbval.denote2	$$⊢\forall x\exists yy=x$$
	bj-cbval.equcomiv	$$⊢y=x\to x=y$$
	bj-cbval.nf0	$$⊢\phi \to \forall x\phi$$
	bj-cbval.nf1	$$⊢\phi \to \forall y\phi$$
	bj-cbval.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	bj-cbvex	$$⊢\phi \to \left(\exists x\psi \leftrightarrow \exists y\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-cbval.denote	$$⊢\forall y\exists xx=y$$
2		bj-cbval.denote2	$$⊢\forall x\exists yy=x$$
3		bj-cbval.equcomiv	$$⊢y=x\to x=y$$
4		bj-cbval.nf0	$$⊢\phi \to \forall x\phi$$
5		bj-cbval.nf1	$$⊢\phi \to \forall y\phi$$
6		bj-cbval.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
7		ax5d	$$⊢\phi \to \left(\psi \to \forall y\psi \right)$$
8	2	a1i	$$⊢\phi \to \forall x\exists yy=x$$
9	3 6	sylan2	$$⊢\left(\phi \wedge y=x\right)\to \left(\psi \leftrightarrow \chi \right)$$
10	9	biimpd	$$⊢\left(\phi \wedge y=x\right)\to \left(\psi \to \chi \right)$$
11	4 5 7 8 10	bj-cbveximdv	$$⊢\phi \to \left(\exists x\psi \to \exists y\chi \right)$$
12		ax5d	$$⊢\phi \to \left(\chi \to \forall x\chi \right)$$
13	1	a1i	$$⊢\phi \to \forall y\exists xx=y$$
14	6	biimprd	$$⊢\left(\phi \wedge x=y\right)\to \left(\chi \to \psi \right)$$
15	5 4 12 13 14	bj-cbveximdv	$$⊢\phi \to \left(\exists y\chi \to \exists x\psi \right)$$
16	11 15	impbid	$$⊢\phi \to \left(\exists x\psi \leftrightarrow \exists y\chi \right)$$