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 -> ( ph <-> ps ) )
Assertion	notabw	|- { x | -. ph } = ( _V \ { y | ps } )

Proof

Step	Hyp	Ref	Expression
1		notabw.1	|- ( x = y -> ( ph <-> ps ) )
2		vex	|- x e. _V
3	2	biantrur	|- ( -. x e. { y | ps } <-> ( x e. _V /\ -. x e. { y | ps } ) )
4		df-clab	|- ( x e. { y | ps } <-> [ x / y ] ps )
5	1	bicomd	|- ( x = y -> ( ps <-> ph ) )
6	5	equcoms	|- ( y = x -> ( ps <-> ph ) )
7	6	sbievw	|- ( [ x / y ] ps <-> ph )
8	4 7	bitri	|- ( x e. { y | ps } <-> ph )
9	3 8	xchnxbi	|- ( -. ph <-> ( x e. _V /\ -. x e. { y | ps } ) )
10	9	abbii	|- { x | -. ph } = { x | ( x e. _V /\ -. x e. { y | ps } ) }
11		df-dif	|- ( _V \ { y | ps } ) = { x | ( x e. _V /\ -. x e. { y | ps } ) }
12	10 11	eqtr4i	|- { x | -. ph } = ( _V \ { y | ps } )