This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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