Theorem bj-cbvaew

Description: Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	|- ( ph <-> -. -. ph )
2	1	albii	|- ( A. x ph <-> A. x -. -. ph )
3		df-fal	|- ( F. <-> -. T. )
4	3	albii	|- ( A. y F. <-> A. y -. T. )
5	2 4	imbi12i	|- ( ( A. x ph -> A. y F. ) <-> ( A. x -. -. ph -> A. y -. T. ) )
6		bj-exexalal	|- ( ( E. y T. -> E. x -. ph ) <-> ( A. x -. -. ph -> A. y -. T. ) )
7	5 6	bitr4i	|- ( ( A. x ph -> A. y F. ) <-> ( E. y T. -> E. x -. ph ) )
8		bj-cbvew	|- ( ( E. y T. -> E. x -. ph ) -> ( E. y ps -> E. x ps ) )
9	7 8	sylbi	|- ( ( A. x ph -> A. y F. ) -> ( E. y ps -> E. x ps ) )