Theorem bj-cbveaw

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

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

Proof

Step	Hyp	Ref	Expression
1		empty	|- ( -. E. x T. <-> A. x F. )
2		falim	|- ( F. -> ps )
3	2	alimi	|- ( A. x F. -> A. x ps )
4	3	a1d	|- ( A. x F. -> ( A. y ps -> A. x ps ) )
5	1 4	sylbi	|- ( -. E. x T. -> ( A. y ps -> A. x ps ) )
6		bj-cbvalvv	|- ( E. y ph -> ( A. y ps -> A. x ps ) )
7	5 6	ja	|- ( ( E. x T. -> E. y ph ) -> ( A. y ps -> A. x ps ) )