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