Step |
Hyp |
Ref |
Expression |
1 |
|
eleq12 |
|- ( ( y = { x e. A | -. x e. x } /\ y = { x e. A | -. x e. x } ) -> ( y e. y <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
2 |
1
|
anidms |
|- ( y = { x e. A | -. x e. x } -> ( y e. y <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
3 |
2
|
notbid |
|- ( y = { x e. A | -. x e. x } -> ( -. y e. y <-> -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
4 |
|
eleq12 |
|- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) ) |
5 |
4
|
anidms |
|- ( x = y -> ( x e. x <-> y e. y ) ) |
6 |
5
|
notbid |
|- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
7 |
6
|
cbvrabv |
|- { x e. A | -. x e. x } = { y e. A | -. y e. y } |
8 |
3 7
|
elrab2 |
|- ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
9 |
|
pclem6 |
|- ( ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) -> -. { x e. A | -. x e. x } e. A ) |
10 |
8 9
|
ax-mp |
|- -. { x e. A | -. x e. x } e. A |