Theorem notabw

Description: A class abstraction defined by a negation. Version of notab using implicit substitution, which does not require ax-10 , ax-12 . (Contributed by Gino Giotto, 15-Oct-2024)

	Ref	Expression
Hypothesis	notabw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	notabw	$$⊢\left\{x|\neg \phi \right\}=\mathrm{V}\setminus \left\{y|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		notabw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	biantrur	$$⊢\neg x\in \left\{y|\psi \right\}\leftrightarrow \left(x\in \mathrm{V}\wedge \neg x\in \left\{y|\psi \right\}\right)$$
4		df-clab	$$⊢x\in \left\{y|\psi \right\}\leftrightarrow \left[x/y\right]\psi$$
5	1	bicomd	$$⊢x=y\to \left(\psi \leftrightarrow \phi \right)$$
6	5	equcoms	$$⊢y=x\to \left(\psi \leftrightarrow \phi \right)$$
7	6	sbievw	$$⊢\left[x/y\right]\psi \leftrightarrow \phi$$
8	4 7	bitri	$$⊢x\in \left\{y|\psi \right\}\leftrightarrow \phi$$
9	3 8	xchnxbi	$$⊢\neg \phi \leftrightarrow \left(x\in \mathrm{V}\wedge \neg x\in \left\{y|\psi \right\}\right)$$
10	9	abbii	$$⊢\left\{x|\neg \phi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \neg x\in \left\{y|\psi \right\}\right)\right\}$$
11		df-dif	$$⊢\mathrm{V}\setminus \left\{y|\psi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \neg x\in \left\{y|\psi \right\}\right)\right\}$$
12	10 11	eqtr4i	$$⊢\left\{x|\neg \phi \right\}=\mathrm{V}\setminus \left\{y|\psi \right\}$$