Theorem bj-exexalal

Description: A lemma for changing bound variables. Only the forward implication is intuitionistic. (Contributed by BJ, 14-Mar-2026)

	Ref	Expression
Assertion	bj-exexalal	|- ( ( E. x ph -> E. y ps ) <-> ( A. y -. ps -> A. x -. ph ) )

Proof

Step	Hyp	Ref	Expression
1		con34b	|- ( ( E. x ph -> E. y ps ) <-> ( -. E. y ps -> -. E. x ph ) )
2		alnex	|- ( A. y -. ps <-> -. E. y ps )
3		alnex	|- ( A. x -. ph <-> -. E. x ph )
4	2 3	imbi12i	|- ( ( A. y -. ps -> A. x -. ph ) <-> ( -. E. y ps -> -. E. x ph ) )
5	1 4	bitr4i	|- ( ( E. x ph -> E. y ps ) <-> ( A. y -. ps -> A. x -. ph ) )