Metamath Proof Explorer


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 } )