Theorem nfabdw

Description: Bound-variable hypothesis builder for a class abstraction. Version of nfabd with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024) (Proof shortened by Wolf Lammen, 23-Sep-2024)

	Ref	Expression
Hypotheses	nfabdw.1	|- F/ y ph
	nfabdw.2	|- ( ph -> F/ x ps )
Assertion	nfabdw	|- ( ph -> F/_ x { y | ps } )

Proof

Step	Hyp	Ref	Expression
1		nfabdw.1	|- F/ y ph
2		nfabdw.2	|- ( ph -> F/ x ps )
3		nfv	|- F/ z ph
4		df-clab	|- ( z e. { y | ps } <-> [ z / y ] ps )
5		sb6	|- ( [ z / y ] ps <-> A. y ( y = z -> ps ) )
6	4 5	bitri	|- ( z e. { y | ps } <-> A. y ( y = z -> ps ) )
7		nfvd	|- ( ph -> F/ x y = z )
8	7 2	nfimd	|- ( ph -> F/ x ( y = z -> ps ) )
9	1 8	nfald	|- ( ph -> F/ x A. y ( y = z -> ps ) )
10	6 9	nfxfrd	|- ( ph -> F/ x z e. { y | ps } )
11	3 10	nfcd	|- ( ph -> F/_ x { y | ps } )