Metamath Proof Explorer


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 syl5bb
 |-  ( 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 )