Theorem bj-alnnf2

Description: If a proposition holds, then it holds for all values of a given variable if and only if it does not depend on that variable. (Contributed by BJ, 28-Mar-2026)

	Ref	Expression
Assertion	bj-alnnf2	|- ( ph -> ( A. x ph <-> F// x ph ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alnnf	|- ( ( ph -> A. x ph ) <-> ( ph -> F// x ph ) )
2	1	pm5.74ri	|- ( ph -> ( A. x ph <-> F// x ph ) )