Metamath Proof Explorer


Theorem nfa1w

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

Ref Expression
Hypothesis nfa1w.x x = y φ ψ
Assertion nfa1w x x φ

Proof

Step Hyp Ref Expression
1 nfa1w.x x = y φ ψ
2 1 cbvalvw x φ y ψ
3 nfv x y ψ
4 2 3 nfxfr x x φ