Theorem bj-denot 32662

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

Assertion

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

Distinct variable group:   x, y

Proof of Theorem bj-denot

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

Syntax hints:   -. wn 3   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-6 1888

This theorem is referenced by: (None)