Metamath Proof Explorer

Theorem bj-denot

Description: A weakening of ax-6 and ax6v . (Contributed by BJ, 4-Apr-2021) (New usage is discouraged.)

Ref Expression
Assertion bj-denot 
|- ( x = x -> -. A. y -. y = x )

Proof

Step Hyp Ref Expression
1 ax6v 
 |-  -. A. y -. y = x
2 1 a1i 
 |-  ( x = x -> -. A. y -. y = x )