Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ovprc1.1 | |- Rel dom F |
|
| Assertion | ovprc1 | |- ( -. A e. _V -> ( A F B ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovprc1.1 | |- Rel dom F |
|
| 2 | simpl | |- ( ( A e. _V /\ B e. _V ) -> A e. _V ) |
|
| 3 | 1 | ovprc | |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) ) |
| 4 | 2 3 | nsyl5 | |- ( -. A e. _V -> ( A F B ) = (/) ) |