Theorem wl-equsb3

Description: equsb3 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019)

	Ref	Expression
Assertion	wl-equsb3	|- ( -. A. y y = z -> ( [ x / y ] y = z <-> x = z ) )

Proof

Step	Hyp	Ref	Expression
1		nfna1	|- F/ y -. A. y y = z
2		nfeqf2	|- ( -. A. y y = z -> F/ y w = z )
3		equequ1	|- ( y = w -> ( y = z <-> w = z ) )
4	3	a1i	|- ( -. A. y y = z -> ( y = w -> ( y = z <-> w = z ) ) )
5	1 2 4	sbied	|- ( -. A. y y = z -> ( [ w / y ] y = z <-> w = z ) )
6	5	sbbidv	|- ( -. A. y y = z -> ( [ x / w ] [ w / y ] y = z <-> [ x / w ] w = z ) )
7		sbco2vv	|- ( [ x / w ] [ w / y ] y = z <-> [ x / y ] y = z )
8		equsb3	|- ( [ x / w ] w = z <-> x = z )
9	6 7 8	3bitr3g	|- ( -. A. y y = z -> ( [ x / y ] y = z <-> x = z ) )