Description: The value of an operation when the one of the arguments is a proper class, analogous to ovprc . (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | aovprc.1 | |- Rel dom F |
|
| Assertion | aovprc | |- ( -. ( A e. _V /\ B e. _V ) -> (( A F B )) = _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aovprc.1 | |- Rel dom F |
|
| 2 | df-aov | |- (( 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 | ndmafv | |- ( -. <. A , B >. e. dom F -> ( F ''' <. A , B >. ) = _V ) |
|
| 7 | 5 6 | nsyl5 | |- ( -. ( A e. _V /\ B e. _V ) -> ( F ''' <. A , B >. ) = _V ) |
| 8 | 2 7 | syl5eq | |- ( -. ( A e. _V /\ B e. _V ) -> (( A F B )) = _V ) |