Description: If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | aovovn0oveq | |- ( ( A F B ) =/= (/) -> (( A F B )) = ( A F B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ov | |- ( A F B ) = ( F ` <. A , B >. ) |
|
| 2 | 1 | neeq1i | |- ( ( A F B ) =/= (/) <-> ( F ` <. A , B >. ) =/= (/) ) |
| 3 | afvfvn0fveq | |- ( ( F ` <. A , B >. ) =/= (/) -> ( F ''' <. A , B >. ) = ( F ` <. A , B >. ) ) |
|
| 4 | df-aov | |- (( A F B )) = ( F ''' <. A , B >. ) |
|
| 5 | 3 4 1 | 3eqtr4g | |- ( ( F ` <. A , B >. ) =/= (/) -> (( A F B )) = ( A F B ) ) |
| 6 | 2 5 | sylbi | |- ( ( A F B ) =/= (/) -> (( A F B )) = ( A F B ) ) |