Description: Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rab0 | |- { x e. (/) | ph } = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rab | |- { x e. (/) | ph } = { x | ( x e. (/) /\ ph ) } |
|
| 2 | ab0 | |- ( { x | ( x e. (/) /\ ph ) } = (/) <-> A. x -. ( x e. (/) /\ ph ) ) |
|
| 3 | noel | |- -. x e. (/) |
|
| 4 | 3 | intnanr | |- -. ( x e. (/) /\ ph ) |
| 5 | 2 4 | mpgbir | |- { x | ( x e. (/) /\ ph ) } = (/) |
| 6 | 1 5 | eqtri | |- { x e. (/) | ph } = (/) |