Theorem nfa1w

Description: Replace ax-10 in nfa1 with a substitution hypothesis. (Contributed by SN, 2-Sep-2025)

	Ref	Expression
Hypothesis	nfa1w.x	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	nfa1w	⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfa1w.x	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	cbvalvw	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )
3		nfv	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜓
4	2 3	nfxfr	⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑