Theorem bj-cbval

Description: Changing a bound variable (universal 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-cbval	|- ( ph -> ( A. x ps <-> A. 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		ax5e	|- ( E. x ch -> ch )
8	7	a1i	|- ( ph -> ( E. x ch -> ch ) )
9	1	a1i	|- ( ph -> A. y E. x x = y )
10	6	biimpd	|- ( ( ph /\ x = y ) -> ( ps -> ch ) )
11	4 5 8 9 10	bj-cbvalimdv	|- ( ph -> ( A. x ps -> A. y ch ) )
12		ax5e	|- ( E. y ps -> ps )
13	12	a1i	|- ( ph -> ( E. y ps -> ps ) )
14	2	a1i	|- ( ph -> A. x E. y y = x )
15	6	biimprd	|- ( ( ph /\ x = y ) -> ( ch -> ps ) )
16	3 15	sylan2	|- ( ( ph /\ y = x ) -> ( ch -> ps ) )
17	5 4 13 14 16	bj-cbvalimdv	|- ( ph -> ( A. y ch -> A. x ps ) )
18	11 17	impbid	|- ( ph -> ( A. x ps <-> A. y ch ) )