Step |
Hyp |
Ref |
Expression |
1 |
|
onnminsb.1 |
|- ( x = A -> ( ph <-> ps ) ) |
2 |
1
|
elrab |
|- ( A e. { x e. On | ph } <-> ( A e. On /\ ps ) ) |
3 |
|
ssrab2 |
|- { x e. On | ph } C_ On |
4 |
|
onnmin |
|- ( ( { x e. On | ph } C_ On /\ A e. { x e. On | ph } ) -> -. A e. |^| { x e. On | ph } ) |
5 |
3 4
|
mpan |
|- ( A e. { x e. On | ph } -> -. A e. |^| { x e. On | ph } ) |
6 |
2 5
|
sylbir |
|- ( ( A e. On /\ ps ) -> -. A e. |^| { x e. On | ph } ) |
7 |
6
|
ex |
|- ( A e. On -> ( ps -> -. A e. |^| { x e. On | ph } ) ) |
8 |
7
|
con2d |
|- ( A e. On -> ( A e. |^| { x e. On | ph } -> -. ps ) ) |