Theorem wl-dfrabsb

Description: Alternate definition of restricted class abstraction ( df-wl-rab ), using substitution. (Contributed by Wolf Lammen, 28-May-2023)

	Ref	Expression
Assertion	wl-dfrabsb	$$⊢\left\{x:A|\phi \right\}=\left\{y|\left(y\in A\wedge \left[y/x\right]\phi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-wl-rab	$$⊢\left\{x:A|\phi \right\}=\left\{y|\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)\right\}$$
2		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
3	2	anbi2i	$$⊢\left(y\in A\wedge \left[y/x\right]\phi \right)\leftrightarrow \left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)$$
4	3	abbii	$$⊢\left\{y|\left(y\in A\wedge \left[y/x\right]\phi \right)\right\}=\left\{y|\left(y\in A\wedge \forall x\left(x=y\to \phi \right)\right)\right\}$$
5	1 4	eqtr4i	$$⊢\left\{x:A|\phi \right\}=\left\{y|\left(y\in A\wedge \left[y/x\right]\phi \right)\right\}$$