Metamath Proof Explorer

Theorem wl-nfae1

Description: Unlike nfae , this specialized theorem avoids ax-11 . (Contributed by Wolf Lammen, 26-Jun-2019)

Ref Expression
Assertion wl-nfae1 
|- F/ x A. y y = x

Proof

Step Hyp Ref Expression
1 aecom 
 |-  ( A. y y = x <-> A. x x = y )
2 nfa1 
 |-  F/ x A. x x = y
3 1 2 nfxfr 
 |-  F/ x A. y y = x