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	|- A. y E. x x = y
	bj-cbval.denote2	|- A. x E. y y = x
	bj-cbval.equcomiv	|- ( y = x -> x = y )
	bj-cbval.nf0	|- ( ph -> A. x ph )
	bj-cbval.nf1	|- ( ph -> A. y ph )
	bj-cbval.is	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	bj-cbvex	|- ( ph -> ( E. x ps <-> E. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbval.denote	|- A. y E. x x = y
2		bj-cbval.denote2	|- A. x E. y y = x
3		bj-cbval.equcomiv	|- ( y = x -> x = y )
4		bj-cbval.nf0	|- ( ph -> A. x ph )
5		bj-cbval.nf1	|- ( ph -> A. y ph )
6		bj-cbval.is	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
7		ax5d	|- ( ph -> ( ps -> A. y ps ) )
8	2	a1i	|- ( ph -> A. x E. y y = x )
9	3 6	sylan2	|- ( ( ph /\ y = x ) -> ( ps <-> ch ) )
10	9	biimpd	|- ( ( ph /\ y = x ) -> ( ps -> ch ) )
11	4 5 7 8 10	bj-cbveximdv	|- ( ph -> ( E. x ps -> E. y ch ) )
12		ax5d	|- ( ph -> ( ch -> A. x ch ) )
13	1	a1i	|- ( ph -> A. y E. x x = y )
14	6	biimprd	|- ( ( ph /\ x = y ) -> ( ch -> ps ) )
15	5 4 12 13 14	bj-cbveximdv	|- ( ph -> ( E. y ch -> E. x ps ) )
16	11 15	impbid	|- ( ph -> ( E. x ps <-> E. y ch ) )