Metamath Proof Explorer

Theorem bj-hbnaeb

Description: Biconditional version of hbnae (to replace it?). (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-hbnaeb 
|- ( -. A. x x = y <-> A. z -. A. x x = y )

Proof

Step Hyp Ref Expression
1 hbnae 
 |-  ( -. A. x x = y -> A. z -. A. x x = y )
2 sp 
 |-  ( A. z -. A. x x = y -> -. A. x x = y )
3 1 2 impbii 
 |-  ( -. A. x x = y <-> A. z -. A. x x = y )