Theorem wl-dfclab

Description: Rederive df-clab from wl-clabv . (Contributed by Wolf Lammen, 31-May-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	wl-dfclab	|- ( x e. { y | ph } <-> [ x / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) )
2		wl-clabv	|- ( z e. { y | ph } <-> [ z / y ] ph )
3		sbequ	|- ( z = x -> ( [ z / y ] ph <-> [ x / y ] ph ) )
4	2 3	bitrid	|- ( z = x -> ( z e. { y | ph } <-> [ x / y ] ph ) )
5	4	pm5.32i	|- ( ( z = x /\ z e. { y | ph } ) <-> ( z = x /\ [ x / y ] ph ) )
6	5	exbii	|- ( E. z ( z = x /\ z e. { y | ph } ) <-> E. z ( z = x /\ [ x / y ] ph ) )
7		19.41v	|- ( E. z ( z = x /\ [ x / y ] ph ) <-> ( E. z z = x /\ [ x / y ] ph ) )
8		ax6ev	|- E. z z = x
9	8	biantrur	|- ( [ x / y ] ph <-> ( E. z z = x /\ [ x / y ] ph ) )
10	7 9	bitr4i	|- ( E. z ( z = x /\ [ x / y ] ph ) <-> [ x / y ] ph )
11	1 6 10	3bitri	|- ( x e. { y | ph } <-> [ x / y ] ph )