Theorem bj-alnnf

Description: In deduction-style proofs, it is equivalent to assert that the context holds for all values of a variable, or that is does not depend on that variable. (Contributed by BJ, 28-Mar-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1	|- ( ph -> ( E. x ph -> ph ) )
2	1	biantrur	|- ( ( ph -> ( ph -> A. x ph ) ) <-> ( ( ph -> ( E. x ph -> ph ) ) /\ ( ph -> ( ph -> A. x ph ) ) ) )
3		pm5.4	|- ( ( ph -> ( ph -> A. x ph ) ) <-> ( ph -> A. x ph ) )
4		pm4.76	|- ( ( ( ph -> ( E. x ph -> ph ) ) /\ ( ph -> ( ph -> A. x ph ) ) ) <-> ( ph -> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) )
5	2 3 4	3bitr3i	|- ( ( ph -> A. x ph ) <-> ( ph -> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) )
6		df-bj-nnf	|- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
7	6	imbi2i	|- ( ( ph -> F// x ph ) <-> ( ph -> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) ) )
8	5 7	bitr4i	|- ( ( ph -> A. x ph ) <-> ( ph -> F// x ph ) )