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	$$⊢Ⅎy\phi$$
	nfabdw.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfabdw.1	$$⊢Ⅎy\phi$$
2		nfabdw.2	$$⊢\phi \to Ⅎx\psi$$
3		nfv	$$⊢Ⅎz\phi$$
4		df-clab	$$⊢z\in \left\{y|\psi \right\}\leftrightarrow \left[z/y\right]\psi$$
5		sb6	$$⊢\left[z/y\right]\psi \leftrightarrow \forall y\left(y=z\to \psi \right)$$
6	4 5	bitri	$$⊢z\in \left\{y|\psi \right\}\leftrightarrow \forall y\left(y=z\to \psi \right)$$
7		nfvd	$$⊢\phi \to Ⅎxy=z$$
8	7 2	nfimd	$$⊢\phi \to Ⅎx\left(y=z\to \psi \right)$$
9	1 8	nfald	$$⊢\phi \to Ⅎx\forall y\left(y=z\to \psi \right)$$
10	6 9	nfxfrd	$$⊢\phi \to Ⅎxz\in \left\{y|\psi \right\}$$
11	3 10	nfcd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$