Theorem wl-clabt

Description: Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv . (Contributed by Wolf Lammen, 29-May-2023)

	Ref	Expression
Hypothesis	wl-clabt.nf	|- F/ x ph
Assertion	wl-clabt	|- ( ph -> { x | ps } = { x | ( ph -> ps ) } )

Proof

Step	Hyp	Ref	Expression
1		wl-clabt.nf	|- F/ x ph
2		biimt	|- ( ph -> ( ps <-> ( ph -> ps ) ) )
3	1 2	sbbid	|- ( ph -> ( [ y / x ] ps <-> [ y / x ] ( ph -> ps ) ) )
4		df-clab	|- ( y e. { x | ps } <-> [ y / x ] ps )
5		df-clab	|- ( y e. { x | ( ph -> ps ) } <-> [ y / x ] ( ph -> ps ) )
6	3 4 5	3bitr4g	|- ( ph -> ( y e. { x | ps } <-> y e. { x | ( ph -> ps ) } ) )
7	6	eqrdv	|- ( ph -> { x | ps } = { x | ( ph -> ps ) } )