Metamath Proof Explorer

Theorem wl-nfeqfb

Description: Extend nfeqf to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 nf5r 
 |-  ( F/ x y = z -> ( y = z -> A. x y = z ) )
2 1 imp 
 |-  ( ( F/ x y = z /\ y = z ) -> A. x y = z )
3 wl-aleq 
 |-  ( A. x y = z <-> ( y = z /\ ( A. x x = y <-> A. x x = z ) ) )
4 3 simprbi 
 |-  ( A. x y = z -> ( A. x x = y <-> A. x x = z ) )
5 2 4 syl 
 |-  ( ( F/ x y = z /\ y = z ) -> ( A. x x = y <-> A. x x = z ) )
6 nfnt 
 |-  ( F/ x y = z -> F/ x -. y = z )
7 6 nf5rd 
 |-  ( F/ x y = z -> ( -. y = z -> A. x -. y = z ) )
8 7 imp 
 |-  ( ( F/ x y = z /\ -. y = z ) -> A. x -. y = z )
9 alnex 
 |-  ( A. x -. y = z <-> -. E. x y = z )
10 wl-exeq 
 |-  ( E. x y = z <-> ( y = z \/ A. x x = y \/ A. x x = z ) )
11 9 10 xchbinx 
 |-  ( A. x -. y = z <-> -. ( y = z \/ A. x x = y \/ A. x x = z ) )
12 3ioran 
 |-  ( -. ( y = z \/ A. x x = y \/ A. x x = z ) <-> ( -. y = z /\ -. A. x x = y /\ -. A. x x = z ) )
13 11 12 sylbb 
 |-  ( A. x -. y = z -> ( -. y = z /\ -. A. x x = y /\ -. A. x x = z ) )
14 3simpc 
 |-  ( ( -. y = z /\ -. A. x x = y /\ -. A. x x = z ) -> ( -. A. x x = y /\ -. A. x x = z ) )
15 pm5.21 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. x x = y <-> A. x x = z ) )
16 8 13 14 15 4syl 
 |-  ( ( F/ x y = z /\ -. y = z ) -> ( A. x x = y <-> A. x x = z ) )
17 5 16 pm2.61dan 
 |-  ( F/ x y = z -> ( A. x x = y <-> A. x x = z ) )
18 ax7 
 |-  ( x = y -> ( x = z -> y = z ) )
19 18 al2imi 
 |-  ( A. x x = y -> ( A. x x = z -> A. x y = z ) )
20 nftht 
 |-  ( A. x y = z -> F/ x y = z )
21 19 20 syl6 
 |-  ( A. x x = y -> ( A. x x = z -> F/ x y = z ) )
22 nfeqf 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y = z )
23 22 ex 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> F/ x y = z ) )
24 21 23 bija 
 |-  ( ( A. x x = y <-> A. x x = z ) -> F/ x y = z )
25 17 24 impbii 
 |-  ( F/ x y = z <-> ( A. x x = y <-> A. x x = z ) )