Description: The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ovprc1.1 | |- Rel dom F |
|
| Assertion | ovprc | |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ovprc1.1 | |- Rel dom F |
|
| 2 | df-ov | |- ( A F B ) = ( F ` <. A , B >. ) |
|
| 3 | df-br | |- ( A dom F B <-> <. A , B >. e. dom F ) |
|
| 4 | 1 | brrelex12i | |- ( A dom F B -> ( A e. _V /\ B e. _V ) ) |
| 5 | 3 4 | sylbir | |- ( <. A , B >. e. dom F -> ( A e. _V /\ B e. _V ) ) |
| 6 | ndmfv | |- ( -. <. A , B >. e. dom F -> ( F ` <. A , B >. ) = (/) ) |
|
| 7 | 5 6 | nsyl5 | |- ( -. ( A e. _V /\ B e. _V ) -> ( F ` <. A , B >. ) = (/) ) |
| 8 | 2 7 | syl5eq | |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) ) |