Description: A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015) (Revised by Mario Carneiro, 15-May-2015) (Proof shortened by AV, 27-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mpo0v | |- ( x e. (/) , y e. B |-> C ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- (/) = (/) |
|
| 2 | 1 | orci | |- ( (/) = (/) \/ B = (/) ) |
| 3 | 0mpo0 | |- ( ( (/) = (/) \/ B = (/) ) -> ( x e. (/) , y e. B |-> C ) = (/) ) |
|
| 4 | 2 3 | ax-mp | |- ( x e. (/) , y e. B |-> C ) = (/) |