Metamath Proof Explorer

Theorem nfeqf2

Description: An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Wolf Lammen, 9-Jun-2019) Remove dependency on ax-12 . (Revised by Wolf Lammen, 16-Dec-2022) (New usage is discouraged.)

Ref Expression
Assertion nfeqf2 
|- ( -. A. x x = y -> F/ x z = y )

Proof

Step Hyp Ref Expression
1 exnal 
 |-  ( E. x -. x = y <-> -. A. x x = y )
2 hbe1 
 |-  ( E. x z = y -> A. x E. x z = y )
3 ax13lem2 
 |-  ( -. x = y -> ( E. x z = y -> z = y ) )
4 ax13lem1 
 |-  ( -. x = y -> ( z = y -> A. x z = y ) )
5 3 4 syldc 
 |-  ( E. x z = y -> ( -. x = y -> A. x z = y ) )
6 2 5 eximdh 
 |-  ( E. x z = y -> ( E. x -. x = y -> E. x A. x z = y ) )
7 hbe1a 
 |-  ( E. x A. x z = y -> A. x z = y )
8 6 7 syl6com 
 |-  ( E. x -. x = y -> ( E. x z = y -> A. x z = y ) )
9 8 nfd 
 |-  ( E. x -. x = y -> F/ x z = y )
10 1 9 sylbir 
 |-  ( -. A. x x = y -> F/ x z = y )