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 -> ( ph <-> ps ) )
Assertion nfa1w 
|- F/ x A. x ph

Proof

Step Hyp Ref Expression
1 nfa1w.x 
 |-  ( x = y -> ( ph <-> ps ) )
2 1 cbvalvw 
 |-  ( A. x ph <-> A. y ps )
3 nfv 
 |-  F/ x A. y ps
4 2 3 nfxfr 
 |-  F/ x A. x ph